:: INCPROJ semantic presentation begin definitionlet "CPS" be ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::); :: original: :::"LINE"::: redefine mode :::"LINE"::: "of" "CPS" -> ($#m1_subset_1 :::"Subset":::) "of" "CPS"; end; definitionlet "CPS" be ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::); func :::"ProjectiveLines"::: "CPS" -> ($#m1_hidden :::"set"::: ) equals :: INCPROJ:def 1 "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" "CPS" : (Bool (Set (Var "B")) "is" ($#m1_incproj :::"LINE"::: ) "of" "CPS") "}" ; end; :: deftheorem defines :::"ProjectiveLines"::: INCPROJ:def 1 : (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) "holds" (Bool (Set ($#k1_incproj :::"ProjectiveLines"::: ) (Set (Var "CPS"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "CPS")) : (Bool (Set (Var "B")) "is" ($#m1_incproj :::"LINE"::: ) "of" (Set (Var "CPS"))) "}" )); registrationlet "CPS" be ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::); cluster (Set ($#k1_incproj :::"ProjectiveLines"::: ) "CPS") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: INCPROJ:1 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_incproj :::"LINE"::: ) "of" (Set (Var "CPS"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_incproj :::"ProjectiveLines"::: ) (Set (Var "CPS")))) ")" ))) ; definitionlet "CPS" be ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::); func :::"Proj_Inc"::: "CPS" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPS") "," (Set "(" ($#k1_incproj :::"ProjectiveLines"::: ) "CPS" ")" ) means :: INCPROJ:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPS")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_incproj :::"ProjectiveLines"::: ) "CPS")) & (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Proj_Inc"::: INCPROJ:def 2 : (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPS"))) "," (Set "(" ($#k1_incproj :::"ProjectiveLines"::: ) (Set (Var "CPS")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_incproj :::"Proj_Inc"::: ) (Set (Var "CPS")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPS")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_incproj :::"ProjectiveLines"::: ) (Set (Var "CPS")))) & (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" ) ")" )) ")" ))); definitionlet "CPS" be ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::); func :::"IncProjSp_of"::: "CPS" -> ($#l1_incsp_1 :::"IncProjStr"::: ) equals :: INCPROJ:def 3 (Set ($#g1_incsp_1 :::"IncProjStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPS") "," (Set "(" ($#k1_incproj :::"ProjectiveLines"::: ) "CPS" ")" ) "," (Set "(" ($#k2_incproj :::"Proj_Inc"::: ) "CPS" ")" ) "#)" ); end; :: deftheorem defines :::"IncProjSp_of"::: INCPROJ:def 3 : (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) "holds" (Bool (Set ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS"))) ($#r1_hidden :::"="::: ) (Set ($#g1_incsp_1 :::"IncProjStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPS"))) "," (Set "(" ($#k1_incproj :::"ProjectiveLines"::: ) (Set (Var "CPS")) ")" ) "," (Set "(" ($#k2_incproj :::"Proj_Inc"::: ) (Set (Var "CPS")) ")" ) "#)" ))); registrationlet "CPS" be ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::); cluster (Set ($#k3_incproj :::"IncProjSp_of"::: ) "CPS") -> ($#v1_incsp_1 :::"strict"::: ) ; end; theorem :: INCPROJ:2 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPS")))) & (Bool (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_incproj :::"ProjectiveLines"::: ) (Set (Var "CPS")))) & (Bool (Set "the" ($#u3_incsp_1 :::"Inc"::: ) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_incproj :::"Proj_Inc"::: ) (Set (Var "CPS")))) ")" )) ; theorem :: INCPROJ:3 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" )) ")" ))) ; theorem :: INCPROJ:4 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_incproj :::"LINE"::: ) "of" (Set (Var "CPS"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" )) ")" ))) ; theorem :: INCPROJ:5 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "p9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) (Bool "for" (Set (Var "P9")) "being" ($#m1_incproj :::"LINE"::: ) "of" (Set (Var "CPS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p9"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "P9")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) "iff" (Bool (Set (Var "p9")) ($#r2_hidden :::"in"::: ) (Set (Var "P9"))) ")" )))))) ; theorem :: INCPROJ:6 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "ex" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "st" (Bool "(" (Bool (Set (Var "a9")) ($#r1_hidden :::"<>"::: ) (Set (Var "b9"))) & (Bool (Set (Var "b9")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9"))) & (Bool (Set (Var "c9")) ($#r1_hidden :::"<>"::: ) (Set (Var "a9"))) ")" ))) ; theorem :: INCPROJ:7 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "for" (Set (Var "a9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) (Bool "ex" (Set (Var "b9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "st" (Bool (Set (Var "a9")) ($#r1_hidden :::"<>"::: ) (Set (Var "b9")))))) ; theorem :: INCPROJ:8 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "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 :: INCPROJ:9 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) ")" )))) ; theorem :: INCPROJ:10 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "c9")))) "holds" (Bool "(" (Bool (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) ($#r1_collsp :::"is_collinear"::: ) ) "iff" (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "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 :: INCPROJ:11 (Bool "for" (Set (Var "CPS")) "being" ($#v4_collsp :::"proper"::: ) ($#l1_collsp :::"CollSp":::) "holds" (Bool "not" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "holds" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))))))) ; theorem :: INCPROJ:12 (Bool "for" (Set (Var "CPS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (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 :: INCPROJ:13 (Bool "for" (Set (Var "CPS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (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 "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) ")" ))))) ; theorem :: INCPROJ:14 (Bool "for" (Set (Var "CPS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) (Bool "ex" (Set (Var "p9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "st" (Bool "(" (Bool (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "p9")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "c9")) "," (Set (Var "d9")) "," (Set (Var "p9")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) ")" )) "holds" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) ")" )))) ; theorem :: INCPROJ:15 (Bool "for" (Set (Var "CPS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool (Bool "ex" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "holds" (Bool "(" "not" (Bool (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "s")) ($#r1_collsp :::"is_collinear"::: ) ) "or" "not" (Bool (Set (Var "r")) "," (Set (Var "r1")) "," (Set (Var "s")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )))) "holds" (Bool "ex" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) "or" "not" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) ")" )))) ; theorem :: INCPROJ:16 (Bool "for" (Set (Var "CPS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) (Bool "ex" (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "st" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q1")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "r")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) ")" )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" )(Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) ")" )))))) ; theorem :: INCPROJ:17 (Bool "for" (Set (Var "CPS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q")) "," (Set (Var "r1")) "," (Set (Var "q1")) "," (Set (Var "p")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "st" (Bool (Bool (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r1")) "," (Set (Var "q1")) "," (Set (Var "q")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "r1")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "q1")) "," (Set (Var "p")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "r2")) "," (Set (Var "r1")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r2")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "r1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) ))) "holds" (Bool (Set (Var "r2")) "," (Set (Var "r1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "L")) "," (Set (Var "Q")) "," (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Bool "not" (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "L"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "r")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "R"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "r")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C")))) "holds" (Bool "not" (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C"))))))) ; theorem :: INCPROJ:18 (Bool "for" (Set (Var "CPS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q1"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Set (Var "p3")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p3")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p2")) "," (Set (Var "p3")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "p3")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "q3")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p2")) "," (Set (Var "q2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p3")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "a1")) "," (Set (Var "b2")) "," (Set (Var "a2")) "," (Set (Var "b3")) "," (Set (Var "a3")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "," (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "B3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "a2")) "," (Set (Var "b2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "a3")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "a2")) "," (Set (Var "t")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "r")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "s")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "t")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "r")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "s")) "," (Set (Var "b2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3"))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3")))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O"))))))) ; theorem :: INCPROJ:19 (Bool "for" (Set (Var "CPS")) "being" ($#l1_collsp :::"CollProjectiveSpace":::) "st" (Bool (Bool "(" "for" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "q3")) "," (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "CPS")) "st" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Set (Var "q2")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q2"))) & (Bool (Set (Var "q1")) ($#r1_hidden :::"<>"::: ) (Set (Var "q3"))) & (Bool (Bool "not" (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "q1")) ($#r1_collsp :::"is_collinear"::: ) )) & (Bool (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "p1")) "," (Set (Var "p3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "q1")) "," (Set (Var "q2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "q1")) "," (Set (Var "q3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "q1")) "," (Set (Var "p2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p1")) "," (Set (Var "q3")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p3")) "," (Set (Var "q1")) "," (Set (Var "r2")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p2")) "," (Set (Var "q3")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) ) & (Bool (Set (Var "p3")) "," (Set (Var "q2")) "," (Set (Var "r1")) ($#r1_collsp :::"is_collinear"::: ) )) "holds" (Bool (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#r1_collsp :::"is_collinear"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "B3")) "," (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k3_incproj :::"IncProjSp_of"::: ) (Set (Var "CPS")) ")" ) "st" (Bool (Bool (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "A3")) ($#r1_hidden :::"<>"::: ) (Set (Var "B3"))) & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "b3")) "," (Set (Var "c1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "c2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "b2")) "," (Set (Var "c3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "b3")) "," (Set (Var "c2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "b2")) "," (Set (Var "c1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "c3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c1")) "," (Set (Var "c2")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C3")))) "holds" (Bool (Set (Var "c3")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C3")))))) ; definitionlet "S" be ($#l1_incsp_1 :::"IncProjStr"::: ) ; attr "S" is :::"partial"::: means :: INCPROJ:def 4 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" "S" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" "S" "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"))))); redefine attr "S" is :::"linear"::: means :: INCPROJ:def 5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" "S" (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" "S" "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) ")" ))); end; :: deftheorem defines :::"partial"::: INCPROJ:def 4 : (Bool "for" (Set (Var "S")) "being" ($#l1_incsp_1 :::"IncProjStr"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_incproj :::"partial"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "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"))))) ")" )); :: deftheorem defines :::"linear"::: INCPROJ:def 5 : (Bool "for" (Set (Var "S")) "being" ($#l1_incsp_1 :::"IncProjStr"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_incsp_1 :::"linear"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) ")" ))) ")" )); definitionlet "S" be ($#l1_incsp_1 :::"IncProjStr"::: ) ; attr "S" is :::"up-2-dimensional"::: means :: INCPROJ:def 6 (Bool "not" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"POINT":::) "of" "S" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" "S" "holds" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P")))))); attr "S" is :::"up-3-rank"::: means :: INCPROJ:def 7 (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" "S" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" "S" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (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"))) ")" ))); attr "S" is :::"Vebleian"::: means :: INCPROJ:def 8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" "S" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" "S" "st" (Bool (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N")))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" "S" "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) ")" )))); end; :: deftheorem defines :::"up-2-dimensional"::: INCPROJ:def 6 : (Bool "for" (Set (Var "S")) "being" ($#l1_incsp_1 :::"IncProjStr"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_incproj :::"up-2-dimensional"::: ) ) "iff" (Bool "not" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P")))))) ")" )); :: deftheorem defines :::"up-3-rank"::: INCPROJ:def 7 : (Bool "for" (Set (Var "S")) "being" ($#l1_incsp_1 :::"IncProjStr"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_incproj :::"up-3-rank"::: ) ) "iff" (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (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"))) ")" ))) ")" )); :: deftheorem defines :::"Vebleian"::: INCPROJ:def 8 : (Bool "for" (Set (Var "S")) "being" ($#l1_incsp_1 :::"IncProjStr"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_incproj :::"Vebleian"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set (Var "d")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (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 "S")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q"))) ")" )))) ")" )); registrationlet "CPS" be ($#l1_collsp :::"CollProjectiveSpace":::); cluster (Set ($#k3_incproj :::"IncProjSp_of"::: ) "CPS") -> ($#v6_incsp_1 :::"linear"::: ) ($#v1_incproj :::"partial"::: ) ($#v2_incproj :::"up-2-dimensional"::: ) ($#v3_incproj :::"up-3-rank"::: ) ($#v4_incproj :::"Vebleian"::: ) ; end; registration cluster ($#v1_incsp_1 :::"strict"::: ) ($#v6_incsp_1 :::"linear"::: ) ($#v1_incproj :::"partial"::: ) ($#v2_incproj :::"up-2-dimensional"::: ) ($#v3_incproj :::"up-3-rank"::: ) ($#v4_incproj :::"Vebleian"::: ) for ($#l1_incsp_1 :::"IncProjStr"::: ) ; end; definitionmode IncProjSp is ($#v6_incsp_1 :::"linear"::: ) ($#v1_incproj :::"partial"::: ) ($#v2_incproj :::"up-2-dimensional"::: ) ($#v3_incproj :::"up-3-rank"::: ) ($#v4_incproj :::"Vebleian"::: ) ($#l1_incsp_1 :::"IncProjStr"::: ) ; end; registrationlet "CPS" be ($#l1_collsp :::"CollProjectiveSpace":::); cluster (Set ($#k3_incproj :::"IncProjSp_of"::: ) "CPS") -> ($#v6_incsp_1 :::"linear"::: ) ($#v1_incproj :::"partial"::: ) ($#v2_incproj :::"up-2-dimensional"::: ) ($#v3_incproj :::"up-3-rank"::: ) ($#v4_incproj :::"Vebleian"::: ) ; end; definitionlet "IT" be ($#l1_incsp_1 :::"IncProjSp":::); attr "IT" is :::"2-dimensional"::: means :: INCPROJ:def 9 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"LINE":::) "of" "IT" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) ")" ))); end; :: deftheorem defines :::"2-dimensional"::: INCPROJ:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#l1_incsp_1 :::"IncProjSp":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_incproj :::"2-dimensional"::: ) ) "iff" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) ")" ))) ")" )); notationlet "IT" be ($#l1_incsp_1 :::"IncProjSp":::); antonym :::"up-3-dimensional"::: "IT" for :::"2-dimensional"::: ; end; definitionlet "IT" be ($#l1_incsp_1 :::"IncProjStr"::: ) ; attr "IT" is :::"at_most-3-dimensional"::: means :: INCPROJ:def 10 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" "IT" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"LINE":::) "of" "IT" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" "IT"(Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"LINE":::) "of" "IT" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) ")" ))))); end; :: deftheorem defines :::"at_most-3-dimensional"::: INCPROJ:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#l1_incsp_1 :::"IncProjStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_incproj :::"at_most-3-dimensional"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IT"))(Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IT")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "N"))) ")" ))))) ")" )); definitionlet "IT" be ($#l1_incsp_1 :::"IncProjSp":::); attr "IT" is :::"3-dimensional"::: means :: INCPROJ:def 11 (Bool "(" (Bool "IT" "is" ($#v6_incproj :::"at_most-3-dimensional"::: ) ) & (Bool "IT" "is" ($#v5_incproj :::"up-3-dimensional"::: ) ) ")" ); end; :: deftheorem defines :::"3-dimensional"::: INCPROJ:def 11 : (Bool "for" (Set (Var "IT")) "being" ($#l1_incsp_1 :::"IncProjSp":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_incproj :::"3-dimensional"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_incproj :::"at_most-3-dimensional"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v5_incproj :::"up-3-dimensional"::: ) ) ")" ) ")" )); definitionlet "IT" be ($#l1_incsp_1 :::"IncProjStr"::: ) ; attr "IT" is :::"Fanoian"::: means :: INCPROJ:def 12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" "IT" (Bool "for" (Set (Var "L")) "," (Set (Var "Q")) "," (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"LINE":::) "of" "IT" "st" (Bool (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Bool "not" (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S")))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "L"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "r")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "R"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "r")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C")))) "holds" (Bool "not" (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))))); end; :: deftheorem defines :::"Fanoian"::: INCPROJ:def 12 : (Bool "for" (Set (Var "IT")) "being" ($#l1_incsp_1 :::"IncProjStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_incproj :::"Fanoian"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "L")) "," (Set (Var "Q")) "," (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "L")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "Q")))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Bool "not" (Set (Var "r")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "R")))) & (Bool (Bool "not" (Set (Var "q")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S")))) & (Bool (Bool "not" (Set (Var "s")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "S")))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "L"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "q")) "," (Set (Var "r")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "Q"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "q")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "R"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "r")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "S"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "q")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "c")) "," (Set (Var "r")) "," (Set (Var "s")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C")))) "holds" (Bool "not" (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C")))))) ")" )); definitionlet "IT" be ($#l1_incsp_1 :::"IncProjStr"::: ) ; attr "IT" is :::"Desarguesian"::: means :: INCPROJ:def 13 (Bool "for" (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "a1")) "," (Set (Var "b2")) "," (Set (Var "a2")) "," (Set (Var "b3")) "," (Set (Var "a3")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"POINT":::) "of" "IT" (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "," (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "B3")) "being" ($#m1_subset_1 :::"LINE":::) "of" "IT" "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "a2")) "," (Set (Var "b2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "a3")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "a2")) "," (Set (Var "t")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "r")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "s")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "t")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "r")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "s")) "," (Set (Var "b2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3"))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3")))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"LINE":::) "of" "IT" "st" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O")))))); end; :: deftheorem defines :::"Desarguesian"::: INCPROJ:def 13 : (Bool "for" (Set (Var "IT")) "being" ($#l1_incsp_1 :::"IncProjStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_incproj :::"Desarguesian"::: ) ) "iff" (Bool "for" (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "a1")) "," (Set (Var "b2")) "," (Set (Var "a2")) "," (Set (Var "b3")) "," (Set (Var "a3")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "," (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "B3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "a2")) "," (Set (Var "b2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "o")) "," (Set (Var "a3")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "a2")) "," (Set (Var "t")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "r")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "s")) "," (Set (Var "a1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "t")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "r")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "s")) "," (Set (Var "b2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a3"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3"))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"<>"::: ) (Set (Var "b2"))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"<>"::: ) (Set (Var "b3")))) "holds" (Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IT")) "st" (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "O")))))) ")" )); definitionlet "IT" be ($#l1_incsp_1 :::"IncProjStr"::: ) ; attr "IT" is :::"Pappian"::: means :: INCPROJ:def 14 (Bool "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#m1_subset_1 :::"POINT":::) "of" "IT" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "B3")) "," (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#m1_subset_1 :::"LINE":::) "of" "IT" "st" (Bool (Bool (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "A3")) ($#r1_hidden :::"<>"::: ) (Set (Var "B3"))) & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "b3")) "," (Set (Var "c1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "c2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "b2")) "," (Set (Var "c3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "b3")) "," (Set (Var "c2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "b2")) "," (Set (Var "c1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "c3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c1")) "," (Set (Var "c2")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C3")))) "holds" (Bool (Set (Var "c3")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C3"))))); end; :: deftheorem defines :::"Pappian"::: INCPROJ:def 14 : (Bool "for" (Set (Var "IT")) "being" ($#l1_incsp_1 :::"IncProjStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_incproj :::"Pappian"::: ) ) "iff" (Bool "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c3")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "B3")) "," (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "o")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "A3")) ($#r1_hidden :::"<>"::: ) (Set (Var "B3"))) & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set (Var "o")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "b3")) "," (Set (Var "c1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "c2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "b2")) "," (Set (Var "c3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C1"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "b3")) "," (Set (Var "c2")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a3")) "," (Set (Var "b2")) "," (Set (Var "c1")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "c3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C2"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "A3"))) & (Bool (Set ($#k8_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k8_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "B3"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "c1")) "," (Set (Var "c2")) ($#k7_domain_1 :::"}"::: ) ) ($#r4_incsp_1 :::"on"::: ) (Set (Var "C3")))) "holds" (Bool (Set (Var "c3")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "C3"))))) ")" )); registration cluster ($#v6_incsp_1 :::"linear"::: ) ($#v1_incproj :::"partial"::: ) ($#v2_incproj :::"up-2-dimensional"::: ) ($#v3_incproj :::"up-3-rank"::: ) ($#v4_incproj :::"Vebleian"::: ) ($#v5_incproj :::"up-3-dimensional"::: ) ($#v6_incproj :::"at_most-3-dimensional"::: ) ($#v8_incproj :::"Fanoian"::: ) ($#v9_incproj :::"Desarguesian"::: ) for ($#l1_incsp_1 :::"IncProjStr"::: ) ; end; registration cluster ($#v6_incsp_1 :::"linear"::: ) ($#v1_incproj :::"partial"::: ) ($#v2_incproj :::"up-2-dimensional"::: ) ($#v3_incproj :::"up-3-rank"::: ) ($#v4_incproj :::"Vebleian"::: ) ($#v5_incproj :::"up-3-dimensional"::: ) ($#v6_incproj :::"at_most-3-dimensional"::: ) ($#v8_incproj :::"Fanoian"::: ) ($#v10_incproj :::"Pappian"::: ) for ($#l1_incsp_1 :::"IncProjStr"::: ) ; end; registration cluster ($#v6_incsp_1 :::"linear"::: ) ($#v1_incproj :::"partial"::: ) ($#v2_incproj :::"up-2-dimensional"::: ) ($#v3_incproj :::"up-3-rank"::: ) ($#v4_incproj :::"Vebleian"::: ) ($#v5_incproj :::"2-dimensional"::: ) ($#v8_incproj :::"Fanoian"::: ) ($#v9_incproj :::"Desarguesian"::: ) for ($#l1_incsp_1 :::"IncProjStr"::: ) ; end; registration cluster ($#v6_incsp_1 :::"linear"::: ) ($#v1_incproj :::"partial"::: ) ($#v2_incproj :::"up-2-dimensional"::: ) ($#v3_incproj :::"up-3-rank"::: ) ($#v4_incproj :::"Vebleian"::: ) ($#v5_incproj :::"2-dimensional"::: ) ($#v8_incproj :::"Fanoian"::: ) ($#v10_incproj :::"Pappian"::: ) for ($#l1_incsp_1 :::"IncProjStr"::: ) ; end;