:: PROJPL_1  semantic presentation begin  


























notationlet "G" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "a" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "G")); let "P" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "G")); antonym "a" :::"|'"::: "P" for "a" :::"on"::: "P"; end; definitionlet "G" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "G")); let "P" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "G")); pred "a" "," "b" :::"|'"::: "P" means :: PROJPL_1:def 1 (Bool  "("  (Bool "a"  ($#r1_incsp_1 :::"|'"::: )  "P") & (Bool "b"  ($#r1_incsp_1 :::"|'"::: )  "P")  ")" ); end; 







:: deftheorem    defines :::"|'"::: PROJPL_1:def 1 :  (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_projpl_1 :::"|'"::: )  (Set (Var "P"))) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "P"))) & (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "P")))  ")" )  ")" )))); 
 definitionlet "G" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "a" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "G")); let "P", "Q" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "G")); pred "a" :::"on"::: "P" "," "Q" means :: PROJPL_1:def 2 (Bool  "("  (Bool "a"  ($#r1_incsp_1 :::"on"::: )  "P") & (Bool "a"  ($#r1_incsp_1 :::"on"::: )  "Q")  ")" ); end; 







:: deftheorem    defines :::"on"::: PROJPL_1:def 2 :  (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q"))) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "Q")))  ")" )  ")" )))); 
 definitionlet "G" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "a" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "G")); let "P", "Q", "R" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "G")); pred "a" :::"on"::: "P" "," "Q" "," "R" means :: PROJPL_1:def 3 (Bool  "("  (Bool "a"  ($#r1_incsp_1 :::"on"::: )  "P") & (Bool "a"  ($#r1_incsp_1 :::"on"::: )  "Q") & (Bool "a"  ($#r1_incsp_1 :::"on"::: )  "R")  ")" ); end; 








:: deftheorem    defines :::"on"::: PROJPL_1:def 3 :  (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r3_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R"))) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "R")))  ")" )  ")" )))); 
 
theorem :: PROJPL_1:1 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "holds"   (Bool  "("   "("  (Bool (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P")))) "implies" (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P")))  ")"  &  "("  (Bool (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P")))) "implies" (Bool  "("  (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q")))) "implies" (Bool (Set (Var "a"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "Q")) "," (Set (Var "P")))  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r3_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")))) "implies" (Bool  "("  (Bool (Set (Var "a"))  ($#r3_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "R")) "," (Set (Var "Q"))) & (Bool (Set (Var "a"))  ($#r3_projpl_1 :::"on"::: )  (Set (Var "Q")) "," (Set (Var "P")) "," (Set (Var "R"))) & (Bool (Set (Var "a"))  ($#r3_projpl_1 :::"on"::: )  (Set (Var "Q")) "," (Set (Var "R")) "," (Set (Var "P"))) & (Bool (Set (Var "a"))  ($#r3_projpl_1 :::"on"::: )  (Set (Var "R")) "," (Set (Var "P")) "," (Set (Var "Q"))) & (Bool (Set (Var "a"))  ($#r3_projpl_1 :::"on"::: )  (Set (Var "R")) "," (Set (Var "Q")) "," (Set (Var "P")))  ")" )  ")"   ")" )))) ; 
 definitionlet "IT" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; attr "IT" is  :::"configuration":::  means :: PROJPL_1:def 4 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" "IT"  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"LINE":::) "of" "IT"  "st" (Bool (Bool (Set (Var "p"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "q"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "p"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Set (Var "q"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q"))))); end; 




:: deftheorem    defines :::"configuration"::: PROJPL_1:def 4 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_projpl_1 :::"configuration"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IT"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "q"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "p"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Set (Var "q"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q")))))  ")" )); 
 
theorem :: PROJPL_1:2 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_projpl_1 :::"configuration"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q")))))  ")" )) ; 
 
theorem :: PROJPL_1:3 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_projpl_1 :::"configuration"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q"))) & (Bool (Set (Var "q"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q"))) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Var "Q")))))  ")" )) ; 
 
theorem :: PROJPL_1:4 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#l1_incsp_1 :::"IncProjSp":::)) "iff" (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_projpl_1 :::"configuration"::: )  ) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "st" (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))))  ")" ) & (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))(Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "p"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "P"))))) & (Bool  "("   "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  ) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "M"))) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "N"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "d")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Set (Var "p"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "P"))) & (Bool (Set (Var "p"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "Q"))) & (Bool (Set (Var "M"))  ($#r1_hidden :::"<>"::: )  (Set (Var "N")))) "holds"  (Bool  "ex" (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "q"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q")))))  ")" )  ")" )  ")" )) ; 
 definitionmode IncProjectivePlane is   ($#v5_incproj :::"2-dimensional"::: )    ($#l1_incsp_1 :::"IncProjSp":::); end; definitionlet "G" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "a", "b", "c" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "G")); pred "a" "," "b" "," "c" :::"is_collinear":::  means :: PROJPL_1:def 5 (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" "G" "st" (Bool (Set  ($#k8_domain_1 :::"{"::: ) "a" "," "b" "," "c" ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P")))); end; 







:: deftheorem    defines :::"is_collinear"::: PROJPL_1:def 5 :  (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_collinear"::: )  ) "iff" (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "st" (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))))  ")" ))); 
 notationlet "G" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "a", "b", "c" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "G")); antonym "a" "," "b" "," "c" :::"is_a_triangle":::  for "a" "," "b" "," "c" :::"is_collinear"::: ; end; 
theorem :: PROJPL_1:5 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_collinear"::: )  ) "iff" (Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set (Var "c"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" ))  ")" ))) ; 
 
theorem :: PROJPL_1:6 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) "iff" (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "P"))) "or" (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "P"))) "or" (Bool (Set (Var "c"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "P")))  ")" ))  ")" ))) ; 
 definitionlet "G" be    ($#l1_incsp_1 :::"IncProjStr"::: )  ; let "a", "b", "c", "d" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "G")); pred "a" "," "b" "," "c" "," "d" :::"is_a_quadrangle":::  means :: PROJPL_1:def 6 (Bool  "("  (Bool "a" "," "b" "," "c"  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool "b" "," "c" "," "d"  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool "c" "," "d" "," "a"  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool "d" "," "a" "," "b"  ($#r4_projpl_1 :::"is_a_triangle"::: )  )  ")" ); end; 








:: deftheorem    defines :::"is_a_quadrangle"::: PROJPL_1:def 6 :  (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  )  ")" )  ")" ))); 
 
theorem :: PROJPL_1:7 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    "st" (Bool (Bool (Set (Var "G")) "is"   ($#l1_incsp_1 :::"IncProjSp":::))) "holds"  (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))))) ; 
 
theorem :: PROJPL_1:8 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "G")) "is"   ($#l1_incsp_1 :::"IncProjSp":::))) "holds"  (Bool  "ex" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "A"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  )  ")" ))))) ; 
 
theorem :: PROJPL_1:9 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "G")) "is"   ($#l1_incsp_1 :::"IncProjSp":::)) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "A"))) & (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "B"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))  ")" ))))) ; 
 
theorem :: PROJPL_1:10 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v1_projpl_1 :::"configuration"::: )  ) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "A"))) & (Bool (Set (Var "a1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a2"))) & (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  )))) ; 
 
theorem :: PROJPL_1:11 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_collinear"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r4_projpl_1 :::"is_collinear"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_collinear"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r4_projpl_1 :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r4_projpl_1 :::"is_collinear"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r4_projpl_1 :::"is_collinear"::: )  )  ")" ))) ; 
 
theorem :: PROJPL_1:12 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  )  ")" ))) ; 
 
theorem :: PROJPL_1:13 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "a")) "," (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set (Var "d")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  )  ")" ))) ; 
 
theorem :: PROJPL_1:14 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v1_projpl_1 :::"configuration"::: )  ) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "A"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "B"))) & (Bool (Set (Var "a1")) "," (Set (Var "a2"))  ($#r1_projpl_1 :::"|'"::: )  (Set (Var "B"))) & (Bool (Set (Var "b1")) "," (Set (Var "b2"))  ($#r1_projpl_1 :::"|'"::: )  (Set (Var "A"))) & (Bool (Set (Var "a1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a2"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b2")))) "holds"  (Bool (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  )))) ; 
 
theorem :: PROJPL_1:15 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    "st" (Bool (Bool (Set (Var "G")) "is"   ($#l1_incsp_1 :::"IncProjSp":::))) "holds"  (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ))) ; 
 definitionlet "G" be   ($#l1_incsp_1 :::"IncProjSp":::); mode  :::"Quadrangle":::  "of" "G" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k4_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "G") "," (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "G") "," (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "G") "," (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" "G") ($#k4_zfmisc_1 :::":]"::: ) ) means :: PROJPL_1:def 7 (Bool (Set it  ($#k4_mcart_1 :::"`1_4"::: )  ) "," (Set it  ($#k5_mcart_1 :::"`2_4"::: )  ) "," (Set it  ($#k6_mcart_1 :::"`3_4"::: )  ) "," (Set it  ($#k7_mcart_1 :::"`4_4"::: )  )  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ); end; 





:: deftheorem    defines :::"Quadrangle"::: PROJPL_1:def 7 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjSp":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k4_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "G"))) "," (Set  "the"  ($#u1_incsp_1 :::"Points"::: )  "of" (Set (Var "G"))) ($#k4_zfmisc_1 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_projpl_1 :::"Quadrangle"::: )   "of" (Set (Var "G"))) "iff" (Bool (Set (Set (Var "b2"))  ($#k4_mcart_1 :::"`1_4"::: )  ) "," (Set (Set (Var "b2"))  ($#k5_mcart_1 :::"`2_4"::: )  ) "," (Set (Set (Var "b2"))  ($#k6_mcart_1 :::"`3_4"::: )  ) "," (Set (Set (Var "b2"))  ($#k7_mcart_1 :::"`4_4"::: )  )  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  )  ")" ))); 
 definitionlet "G" be   ($#l1_incsp_1 :::"IncProjSp":::); let "a", "b" be   ($#m1_subset_1 :::"POINT":::) "of" (Set (Const "G")); assume 
(Bool (Set (Const "a"))  ($#r1_hidden :::"<>"::: )  (Set (Const "b")))
 ; func "a" :::"*"::: "b" ->   ($#m1_subset_1 :::"LINE":::) "of" "G" means :: PROJPL_1:def 8 (Bool (Set  ($#k7_domain_1 :::"{"::: ) "a" "," "b" ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  it); end; 








:: deftheorem    defines :::"*"::: PROJPL_1:def 8 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "b")))) "iff" (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "b4")))  ")" )))); 
 
theorem :: PROJPL_1:16 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "b")))) & (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "b")))) & (Bool (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "a")))) &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L"))) & (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L")))) "implies" (Bool (Set (Var "L"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "b"))))  ")"   ")" )))) ; 
 begin  
theorem :: PROJPL_1:17 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    "st" (Bool (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  )) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "M")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "st" (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "M"))))  ")" )) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))(Bool  "ex" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "p"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "P")))))) ; 
 
theorem :: PROJPL_1:18 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    "st" (Bool (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ))) "holds"  (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ))) ; 
 
theorem :: PROJPL_1:19 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  ) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "Q")))) "holds"  (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Q")))))) ; 
 
theorem :: PROJPL_1:20 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "Q"))) & (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "d")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "R")))) "holds"  (Bool (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  )))) ; 
 
theorem :: PROJPL_1:21 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "," (Set (Var "A")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v1_projpl_1 :::"configuration"::: )  ) & (Bool (Set (Var "a"))  ($#r3_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R"))) & (Bool (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  ) & (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "A"))) & (Bool (Set (Var "p"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "A")) "," (Set (Var "P"))) & (Bool (Set (Var "q"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "A")) "," (Set (Var "Q"))) & (Bool (Set (Var "r"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "A")) "," (Set (Var "R")))) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  )))) ; 
 
theorem :: PROJPL_1:22 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )    "st" (Bool (Bool (Set (Var "G")) "is"   ($#v1_projpl_1 :::"configuration"::: )  ) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "M")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "st" (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "M"))))  ")" ) & (Bool  "("   "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q"))))  ")" ) & (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ))) "holds"  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  ) & (Bool (Set  ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k8_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "P")))  ")" )))) ; 
 
theorem :: PROJPL_1:23 (Bool  "for" (Set (Var "G")) "being"    ($#l1_incsp_1 :::"IncProjStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#l1_incsp_1 :::"IncProjectivePlane":::)) "iff" (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_projpl_1 :::"configuration"::: )  ) & (Bool  "("   "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "M")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) "st" (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k7_domain_1 :::"}"::: ) )  ($#r4_incsp_1 :::"on"::: )  (Set (Var "M"))))  ")" ) & (Bool  "("   "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G")) (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "P")) "," (Set (Var "Q"))))  ")" ) & (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  ))  ")" )  ")" )) ; 
 










definitionlet "G" be   ($#l1_incsp_1 :::"IncProjectivePlane":::); let "A", "B" be   ($#m1_subset_1 :::"LINE":::) "of" (Set (Const "G")); assume 
(Bool (Set (Const "A"))  ($#r1_hidden :::"<>"::: )  (Set (Const "B")))
 ; func "A" :::"*"::: "B" ->   ($#m1_subset_1 :::"POINT":::) "of" "G" means :: PROJPL_1:def 9 (Bool it  ($#r2_projpl_1 :::"on"::: )  "A" "," "B"); end; 








:: deftheorem    defines :::"*"::: PROJPL_1:def 9 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "B")))) "iff" (Bool (Set (Var "b4"))  ($#r2_projpl_1 :::"on"::: )  (Set (Var "A")) "," (Set (Var "B")))  ")" )))); 
 
theorem :: PROJPL_1:24 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "B")))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "A"))) & (Bool (Set (Set (Var "A"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "B")))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "B"))) & (Bool (Set (Set (Var "A"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "A")))) &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "A"))) & (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "B")))) "implies" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "B"))))  ")"   ")" )))) ; 
 
theorem :: PROJPL_1:25 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B"))) & (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "A"))) & (Bool (Set (Var "q"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "A"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "A"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "B"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k2_projpl_1 :::"*"::: )  (Set (Var "B")))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "B"))) & (Bool (Set (Set  "(" (Set (Var "q"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k2_projpl_1 :::"*"::: )  (Set (Var "B")))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "A")))  ")" )))) ; 
 begin  












theorem :: PROJPL_1:26 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r4_projpl_1 :::"is_a_triangle"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  ))) ; 
 
theorem :: PROJPL_1:27 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r5_projpl_1 :::"is_a_quadrangle"::: )  )) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d"))  ($#r2_zfmisc_1 :::"are_mutually_different"::: )  ))) ; 
 



theorem :: PROJPL_1:28 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "d")))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) "or" (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) "or" (Bool (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "d"))))  ")" ))) ; 
 
theorem :: PROJPL_1:29 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "d")))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) "or" (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) "or" (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "c"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "d"))))  ")" ))) ; 
 
theorem :: PROJPL_1:30 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "e")) "," (Set (Var "m")) "," (Set (Var "m9")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "I")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "m"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "I"))) & (Bool (Set (Var "m9"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "I"))) & (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m9"))) & (Bool (Set (Var "e"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "I")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "m"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "e")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "m9"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "e")))) & (Bool (Set (Set (Var "e"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "m")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "e"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "m9"))))  ")" )))) ; 
 
theorem :: PROJPL_1:31 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "I")) "," (Set (Var "L1")) "," (Set (Var "L2")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "e"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L1"))) & (Bool (Set (Var "e"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "L2"))) & (Bool (Set (Var "L1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "L2"))) & (Bool (Set (Var "e"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "I")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "I"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "L1")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "I"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "L2")))) & (Bool (Set (Set (Var "L1"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "I")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "L2"))  ($#k2_projpl_1 :::"*"::: )  (Set (Var "I"))))  ")" )))) ; 
 
theorem :: PROJPL_1:32 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "q1")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "q"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "b")))) & (Bool (Set (Var "q"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "q1")))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "q1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "q1"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "b")))))) ; 
 
theorem :: PROJPL_1:33 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "c"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "b")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "a"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "c")))))) ; 
 
theorem :: PROJPL_1:34 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "r1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "r2"))) & (Bool (Set (Var "r1"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "H"))) & (Bool (Set (Var "r2"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "H"))) & (Bool (Set (Var "q1"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "H"))) & (Bool (Set (Var "q2"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "H")))) "holds"  (Bool (Set (Set (Var "q1"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "r1")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "q2"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "r2"))))))) ; 
 
theorem :: PROJPL_1:35 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "b"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "c")))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "or" (Bool (Set (Var "b"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "c"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "a"))))  ")" ))) ; 
 
theorem :: PROJPL_1:36 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "b"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "c")))) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) "or" (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) "or" (Bool (Set (Var "c"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "b"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "a"))))  ")" ))) ; 
 
theorem :: PROJPL_1:37 (Bool  "for" (Set (Var "G")) "being"   ($#l1_incsp_1 :::"IncProjectivePlane":::)  (Bool  "for" (Set (Var "e")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "H")) "," (Set (Var "I")) "being"   ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "x1"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "I"))) & (Bool (Set (Var "x2"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "I"))) & (Bool (Set (Var "e"))  ($#r1_incsp_1 :::"|'"::: )  (Set (Var "I"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "p1"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "e"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "x1")))) & (Bool (Set (Var "p2"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "e"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "x2"))))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_incsp_1 :::"on"::: )  (Set (Set (Var "p1"))  ($#k1_projpl_1 :::"*"::: )  (Set (Var "p2")))) & (Bool (Set (Var "r"))  ($#r1_incsp_1 :::"on"::: )  (Set (Var "H"))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e")))  ")" ))))) ;