:: AFPROJ semantic presentation begin theorem :: AFPROJ:1 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinPlane":::)) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AS"))))) "holds" (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ))) ; theorem :: AFPROJ:2 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinPlane":::)) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AS")))))) ; theorem :: AFPROJ:3 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinPlane":::)) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))))) ; theorem :: AFPROJ:4 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AS")))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinPlane":::)))) ; theorem :: AFPROJ:5 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "K")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Bool "not" (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "K")))) & (Bool (Set (Var "A")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) & (Bool (Set (Var "A")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) & (Bool (Set (Var "K")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) & (Bool (Set (Var "K")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))))) ; theorem :: AFPROJ:6 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "A")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "A")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"AfLines"::: "AS" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "AS" equals :: AFPROJ:def 1 "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" "AS" : (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) "}" ; end; :: deftheorem defines :::"AfLines"::: AFPROJ:def 1 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k1_afproj :::"AfLines"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) : (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) "}" )); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"AfPlanes"::: "AS" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "AS" equals :: AFPROJ:def 2 "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" "AS" : (Bool (Set (Var "A")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) "}" ; end; :: deftheorem defines :::"AfPlanes"::: AFPROJ:def 2 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k2_afproj :::"AfPlanes"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) : (Bool (Set (Var "A")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) "}" )); theorem :: AFPROJ:7 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_afproj :::"AfLines"::: ) (Set (Var "AS")))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" )) ")" ))) ; theorem :: AFPROJ:8 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_afproj :::"AfPlanes"::: ) (Set (Var "AS")))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" )) ")" ))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"LinesParallelity"::: "AS" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "(" ($#k1_afproj :::"AfLines"::: ) "AS" ")" ) equals :: AFPROJ:def 3 "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "K")) "," (Set (Var "M")) ($#k1_domain_1 :::"]"::: ) ) where K, M "is" ($#m1_subset_1 :::"Subset":::) "of" "AS" : (Bool "(" (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "K")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "M"))) ")" ) "}" ; end; :: deftheorem defines :::"LinesParallelity"::: AFPROJ:def 3 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k3_afproj :::"LinesParallelity"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "K")) "," (Set (Var "M")) ($#k1_domain_1 :::"]"::: ) ) where K, M "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) : (Bool "(" (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "K")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "M"))) ")" ) "}" )); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"PlanesParallelity"::: "AS" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "(" ($#k2_afproj :::"AfPlanes"::: ) "AS" ")" ) equals :: AFPROJ:def 4 "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k1_domain_1 :::"]"::: ) ) where X, Y "is" ($#m1_subset_1 :::"Subset":::) "of" "AS" : (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) ")" ) "}" ; end; :: deftheorem defines :::"PlanesParallelity"::: AFPROJ:def 4 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k4_afproj :::"PlanesParallelity"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k1_domain_1 :::"]"::: ) ) where X, Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) : (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) ")" ) "}" )); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); func :::"LDir"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_afproj :::"AfLines"::: ) "AS" ")" ) equals :: AFPROJ:def 5 (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k3_afproj :::"LinesParallelity"::: ) "AS" ")" ) "," "X" ")" ); end; :: deftheorem defines :::"LDir"::: AFPROJ:def 5 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k3_afproj :::"LinesParallelity"::: ) (Set (Var "AS")) ")" ) "," (Set (Var "X")) ")" )))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "AS")); func :::"PDir"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_afproj :::"AfPlanes"::: ) "AS" ")" ) equals :: AFPROJ:def 6 (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_afproj :::"PlanesParallelity"::: ) "AS" ")" ) "," "X" ")" ); end; :: deftheorem defines :::"PDir"::: AFPROJ:def 6 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "holds" (Bool (Set ($#k6_afproj :::"PDir"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_afproj :::"PlanesParallelity"::: ) (Set (Var "AS")) ")" ) "," (Set (Var "X")) ")" )))); theorem :: AFPROJ:9 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) ")" )) ")" )))) ; theorem :: AFPROJ:10 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_afproj :::"PDir"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) ")" )) ")" )))) ; theorem :: AFPROJ:11 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "(" (Bool (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "Y")))) "iff" (Bool (Set (Var "X")) ($#r5_aff_1 :::"//"::: ) (Set (Var "Y"))) ")" ))) ; theorem :: AFPROJ:12 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "(" (Bool (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "Y")))) "iff" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) ")" ))) ; theorem :: AFPROJ:13 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "(" (Bool (Set ($#k6_afproj :::"PDir"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k6_afproj :::"PDir"::: ) (Set (Var "Y")))) "iff" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) ")" ))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"Dir_of_Lines"::: "AS" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: AFPROJ:def 7 (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k3_afproj :::"LinesParallelity"::: ) "AS" ")" )); end; :: deftheorem defines :::"Dir_of_Lines"::: AFPROJ:def 7 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k7_afproj :::"Dir_of_Lines"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k3_afproj :::"LinesParallelity"::: ) (Set (Var "AS")) ")" )))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"Dir_of_Planes"::: "AS" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: AFPROJ:def 8 (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k4_afproj :::"PlanesParallelity"::: ) "AS" ")" )); end; :: deftheorem defines :::"Dir_of_Planes"::: AFPROJ:def 8 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k8_afproj :::"Dir_of_Planes"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k4_afproj :::"PlanesParallelity"::: ) (Set (Var "AS")) ")" )))); theorem :: AFPROJ:14 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_afproj :::"Dir_of_Lines"::: ) (Set (Var "AS")))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" )) ")" ))) ; theorem :: AFPROJ:15 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_afproj :::"Dir_of_Planes"::: ) (Set (Var "AS")))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_afproj :::"PDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" )) ")" ))) ; theorem :: AFPROJ:16 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AS"))) ($#r1_subset_1 :::"misses"::: ) (Set ($#k7_afproj :::"Dir_of_Lines"::: ) (Set (Var "AS"))))) ; theorem :: AFPROJ:17 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "st" (Bool (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinPlane":::))) "holds" (Bool (Set ($#k1_afproj :::"AfLines"::: ) (Set (Var "AS"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k8_afproj :::"Dir_of_Planes"::: ) (Set (Var "AS"))))) ; theorem :: AFPROJ:18 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_afproj :::"AfLines"::: ) (Set (Var "AS")) ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Num 1) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" )) ")" ))) ; theorem :: AFPROJ:19 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k8_afproj :::"Dir_of_Planes"::: ) (Set (Var "AS")) ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Num 2) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_afproj :::"PDir"::: ) (Set (Var "X")) ")" ) "," (Num 2) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" )) ")" ))) ; definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"ProjectivePoints"::: "AS" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: AFPROJ:def 9 (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AS") ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_afproj :::"Dir_of_Lines"::: ) "AS" ")" )); end; :: deftheorem defines :::"ProjectivePoints"::: AFPROJ:def 9 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k9_afproj :::"ProjectivePoints"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AS"))) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_afproj :::"Dir_of_Lines"::: ) (Set (Var "AS")) ")" )))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"ProjectiveLines"::: "AS" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: AFPROJ:def 10 (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_afproj :::"AfLines"::: ) "AS" ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k8_afproj :::"Dir_of_Planes"::: ) "AS" ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Num 2) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; :: deftheorem defines :::"ProjectiveLines"::: AFPROJ:def 10 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k10_afproj :::"ProjectiveLines"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_afproj :::"AfLines"::: ) (Set (Var "AS")) ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k8_afproj :::"Dir_of_Planes"::: ) (Set (Var "AS")) ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Num 2) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"Proj_Inc"::: "AS" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k9_afproj :::"ProjectivePoints"::: ) "AS" ")" ) "," (Set "(" ($#k10_afproj :::"ProjectiveLines"::: ) "AS" ")" ) means :: AFPROJ:def 11 (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 "ex" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AS" "st" (Bool "(" (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "K")) "," (Num 1) ($#k4_tarski :::"]"::: ) )) & (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AS")) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) ")" ) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "K")))) ")" ) ")" )) "or" (Bool "ex" (Set (Var "K")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AS" "st" (Bool "(" (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "K")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_afproj :::"PDir"::: ) (Set (Var "X")) ")" ) "," (Num 2) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "K")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Proj_Inc"::: AFPROJ:def 11 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k9_afproj :::"ProjectivePoints"::: ) (Set (Var "AS")) ")" ) "," (Set "(" ($#k10_afproj :::"ProjectiveLines"::: ) (Set (Var "AS")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_afproj :::"Proj_Inc"::: ) (Set (Var "AS")))) "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 "ex" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "K")) "," (Num 1) ($#k4_tarski :::"]"::: ) )) & (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AS")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) ")" ) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "K")))) ")" ) ")" )) "or" (Bool "ex" (Set (Var "K")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "K")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_afproj :::"PDir"::: ) (Set (Var "X")) ")" ) "," (Num 2) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "K")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) ")" )) ")" ) ")" )) ")" ))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"Inc_of_Dir"::: "AS" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k7_afproj :::"Dir_of_Lines"::: ) "AS" ")" ) "," (Set "(" ($#k8_afproj :::"Dir_of_Planes"::: ) "AS" ")" ) means :: AFPROJ:def 12 (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 "ex" (Set (Var "A")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AS" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "A")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_afproj :::"PDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "A")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) ")" )) ")" )); end; :: deftheorem defines :::"Inc_of_Dir"::: AFPROJ:def 12 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k7_afproj :::"Dir_of_Lines"::: ) (Set (Var "AS")) ")" ) "," (Set "(" ($#k8_afproj :::"Dir_of_Planes"::: ) (Set (Var "AS")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_afproj :::"Inc_of_Dir"::: ) (Set (Var "AS")))) "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 "ex" (Set (Var "A")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "A")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_afproj :::"PDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "A")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) ")" )) ")" )) ")" ))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"IncProjSp_of"::: "AS" -> ($#v1_incsp_1 :::"strict"::: ) ($#l1_incsp_1 :::"IncProjStr"::: ) equals :: AFPROJ:def 13 (Set ($#g1_incsp_1 :::"IncProjStr"::: ) "(#" (Set "(" ($#k9_afproj :::"ProjectivePoints"::: ) "AS" ")" ) "," (Set "(" ($#k10_afproj :::"ProjectiveLines"::: ) "AS" ")" ) "," (Set "(" ($#k11_afproj :::"Proj_Inc"::: ) "AS" ")" ) "#)" ); end; :: deftheorem defines :::"IncProjSp_of"::: AFPROJ:def 13 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) (Set ($#g1_incsp_1 :::"IncProjStr"::: ) "(#" (Set "(" ($#k9_afproj :::"ProjectivePoints"::: ) (Set (Var "AS")) ")" ) "," (Set "(" ($#k10_afproj :::"ProjectiveLines"::: ) (Set (Var "AS")) ")" ) "," (Set "(" ($#k11_afproj :::"Proj_Inc"::: ) (Set (Var "AS")) ")" ) "#)" ))); definitionlet "AS" be ($#l1_analoaf :::"AffinSpace":::); func :::"ProjHorizon"::: "AS" -> ($#v1_incsp_1 :::"strict"::: ) ($#l1_incsp_1 :::"IncProjStr"::: ) equals :: AFPROJ:def 14 (Set ($#g1_incsp_1 :::"IncProjStr"::: ) "(#" (Set "(" ($#k7_afproj :::"Dir_of_Lines"::: ) "AS" ")" ) "," (Set "(" ($#k8_afproj :::"Dir_of_Planes"::: ) "AS" ")" ) "," (Set "(" ($#k12_afproj :::"Inc_of_Dir"::: ) "AS" ")" ) "#)" ); end; :: deftheorem defines :::"ProjHorizon"::: AFPROJ:def 14 : (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool (Set ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS"))) ($#r1_hidden :::"="::: ) (Set ($#g1_incsp_1 :::"IncProjStr"::: ) "(#" (Set "(" ($#k7_afproj :::"Dir_of_Lines"::: ) (Set (Var "AS")) ")" ) "," (Set "(" ($#k8_afproj :::"Dir_of_Planes"::: ) (Set (Var "AS")) ")" ) "," (Set "(" ($#k12_afproj :::"Inc_of_Dir"::: ) (Set (Var "AS")) ")" ) "#)" ))); theorem :: AFPROJ:20 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" )) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS"))) "or" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" )) ")" ) ")" ))) ; theorem :: AFPROJ:21 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" ))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" )) ")" ))) ; theorem :: AFPROJ:22 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" )))) ; theorem :: AFPROJ:23 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" )) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Num 1) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_afproj :::"PDir"::: ) (Set (Var "X")) ")" ) "," (Num 2) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" ) ")" )) ")" ))) ; theorem :: AFPROJ:24 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" ))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_afproj :::"PDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) ")" )) ")" ))) ; theorem :: AFPROJ:25 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) "is" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" )))) ; theorem :: AFPROJ:26 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )))))) ; theorem :: AFPROJ:27 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_afproj :::"PDir"::: ) (Set (Var "X")) ")" ) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "not" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))))))))) ; theorem :: AFPROJ:28 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "Y")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Var "Y")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "Y")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) ")" ))))) ; theorem :: AFPROJ:29 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "Y")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_afproj :::"PDir"::: ) (Set (Var "X")) ")" ) "," (Num 2) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "Y")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "Y")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "X"))) ")" ))))) ; theorem :: AFPROJ:30 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Num 1) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))))))) ; theorem :: AFPROJ:31 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_afproj :::"PDir"::: ) (Set (Var "Y")) ")" ) "," (Num 2) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))))))) ; theorem :: AFPROJ:32 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "," (Set (Var "X9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X9")) ($#r5_aff_1 :::"//"::: ) (Set (Var "X"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X9")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_afproj :::"PDir"::: ) (Set (Var "Y")) ")" ) "," (Num 2) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))))))) ; theorem :: AFPROJ:33 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k6_afproj :::"PDir"::: ) (Set (Var "X")) ")" ) "," (Num 2) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A")))) "holds" (Bool "not" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")))))))) ; theorem :: AFPROJ:34 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Num 1) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "p")) "is" (Bool "not" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X")))))))) ; theorem :: AFPROJ:35 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "p")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Num 1) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "p")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) "is" (Bool "not" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS"))))) "holds" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS"))))))) ; theorem :: AFPROJ:36 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_afproj :::"LDir"::: ) (Set (Var "X")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k6_afproj :::"PDir"::: ) (Set (Var "Y")))) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "X")) ($#r1_aff_4 :::"'||'"::: ) (Set (Var "Y"))) ")" ))))) ; theorem :: AFPROJ:37 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) (Bool "for" (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" )) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) (Bool "for" (Set (Var "A9")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "A9")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Num 2) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "a9")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A9"))) ")" )))))) ; theorem :: AFPROJ:38 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) (Bool "for" (Set (Var "A")) "," (Set (Var "K")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) "st" (Bool (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "K")))))) ; theorem :: AFPROJ:39 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (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"))) ")" )))) ; theorem :: AFPROJ:40 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_incsp_1 :::"on"::: ) (Set (Var "A"))) ")" )))) ; theorem :: AFPROJ:41 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" )) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "X")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u3_incsp_1 :::"Inc"::: ) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "X")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u3_incsp_1 :::"Inc"::: ) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" )))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) "st" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "Y")) "," (Num 2) ($#k4_tarski :::"]"::: ) )))))) ; theorem :: AFPROJ:42 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u3_incsp_1 :::"Inc"::: ) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" )))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )))))) ; theorem :: AFPROJ:43 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "," (Set (Var "X9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"LINE":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "st" (Bool (Bool (Set (Var "Y")) "is" ($#v1_aff_4 :::"being_plane"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X9")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X9")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Num 1) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X9")) "," (Num 1) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"POINT":::) "of" (Set "(" ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS")) ")" ) "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 :: AFPROJ:44 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_incsp_1 :::"Lines"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) "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 :::"Element"::: ) "of" (Set "the" ($#u1_incsp_1 :::"Points"::: ) "of" (Set "(" ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS")) ")" )) "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 "AS" be ($#l1_analoaf :::"AffinSpace":::); cluster (Set ($#k13_afproj :::"IncProjSp_of"::: ) "AS") -> ($#v1_incsp_1 :::"strict"::: ) ($#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"::: ) ($#v5_incproj :::"2-dimensional"::: ) for ($#l1_incsp_1 :::"IncProjStr"::: ) ; end; registrationlet "AS" be ($#l1_analoaf :::"AffinPlane":::); cluster (Set ($#k13_afproj :::"IncProjSp_of"::: ) "AS") -> ($#v1_incsp_1 :::"strict"::: ) ($#v5_incproj :::"2-dimensional"::: ) ; end; theorem :: AFPROJ:45 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "st" (Bool (Bool (Set ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS"))) "is" ($#v5_incproj :::"2-dimensional"::: ) )) "holds" (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinPlane":::))) ; theorem :: AFPROJ:46 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "st" (Bool (Bool (Set (Var "AS")) "is" (Bool "not" ($#l1_analoaf :::"AffinPlane":::)))) "holds" (Bool (Set ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS"))) "is" ($#l1_incsp_1 :::"IncProjSp":::))) ; theorem :: AFPROJ:47 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "st" (Bool (Bool (Set ($#k14_afproj :::"ProjHorizon"::: ) (Set (Var "AS"))) "is" ($#l1_incsp_1 :::"IncProjSp":::))) "holds" (Bool "not" (Bool (Set (Var "AS")) "is" ($#l1_analoaf :::"AffinPlane":::)))) ; theorem :: AFPROJ:48 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "N")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b9"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "a")) "," (Set (Var "b9")) ($#r2_analoaf :::"//"::: ) (Set (Var "b")) "," (Set (Var "a9"))) & (Bool (Set (Var "b")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "b9"))) & (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )) "holds" (Bool (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9")))))) ; theorem :: AFPROJ:49 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "st" (Bool (Bool (Set ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS"))) "is" ($#v10_incproj :::"Pappian"::: ) )) "holds" (Bool (Set (Var "AS")) "is" ($#v2_aff_2 :::"Pappian"::: ) )) ; theorem :: AFPROJ:50 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AS")) (Bool "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "P")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "P"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool "(" (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) ")" )) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9")))))) ; theorem :: AFPROJ:51 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "st" (Bool (Bool (Set ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS"))) "is" ($#v9_incproj :::"Desarguesian"::: ) )) "holds" (Bool (Set (Var "AS")) "is" ($#v4_aff_2 :::"Desarguesian"::: ) )) ; theorem :: AFPROJ:52 (Bool "for" (Set (Var "AS")) "being" ($#l1_analoaf :::"AffinSpace":::) "st" (Bool (Bool (Set ($#k13_afproj :::"IncProjSp_of"::: ) (Set (Var "AS"))) "is" ($#v8_incproj :::"Fanoian"::: ) )) "holds" (Bool (Set (Var "AS")) "is" ($#v1_translac :::"Fanoian"::: ) )) ;