:: PAPDESAF  semantic presentation begin  registrationlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); 
cluster (Set   ($#k2_diraf :::"Lambda"::: )  "OAS") ->  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v1_diraf :::"AffinSpace-like"::: )   ; 
end; registrationlet "OAS" be   ($#l1_analoaf :::"OAffinPlane":::); 
cluster (Set   ($#k2_diraf :::"Lambda"::: )  "OAS") ->   ($#v2_diraf :::"2-dimensional"::: )   ; 
end; 
theorem :: PAPDESAF:1 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")))) "implies" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS")) ")" ))  ")"  &  "("  (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS")) ")" ))) "implies" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")))  ")"  &  "("  (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "OAS")))) "implies" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS")) ")" ))  ")"  &  "("  (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS")) ")" ))) "implies" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "OAS")))  ")"   ")" ))) ; 
 
theorem :: PAPDESAF:2 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  (Bool  "for" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS")) ")" )  "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   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) "iff" (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")))  ")" )))) ; 
 
theorem :: PAPDESAF:3 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k2_analoaf :::"OASpace"::: )  (Set (Var "V")) ")" )) "iff" (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")))  ")" ))) ; 
 
theorem :: PAPDESAF:4 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analoaf :::"OASpace"::: )  (Set (Var "V"))))) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  (Bool  "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "u"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "v"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "w"))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "holds"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) "iff" (Bool (Set (Var "u")) "," (Set (Var "v"))  ($#r1_geomtrap :::"'||'"::: )  (Set (Var "w")) "," (Set (Var "y")))  ")" ))))) ; 
 
theorem :: PAPDESAF:5 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analoaf :::"OASpace"::: )  (Set (Var "V"))))) "holds"  (Bool  "ex" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "u")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V"))))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))))) ; 
 definitionlet "AS" be   ($#l1_analoaf :::"AffinSpace":::); redefine attr "AS" is  :::"Fanoian":::  means :: PAPDESAF:def 1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AS"  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "c")))); end; 




:: deftheorem    defines :::"Fanoian"::: PAPDESAF:def 1 :  (Bool  "for" (Set (Var "AS")) "being"   ($#l1_analoaf :::"AffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "AS")) "is"   ($#v1_translac :::"Fanoian"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "c"))))  ")" )); 
 definitionlet "IT" be   ($#l1_analoaf :::"OAffinSpace":::); attr "IT" is  :::"Pappian":::  means :: PAPDESAF:def 2 (Bool (Set   ($#k2_diraf :::"Lambda"::: )  "IT") "is"   ($#v2_aff_2 :::"Pappian"::: )  ); attr "IT" is  :::"Desarguesian":::  means :: PAPDESAF:def 3 (Bool (Set   ($#k2_diraf :::"Lambda"::: )  "IT") "is"   ($#v4_aff_2 :::"Desarguesian"::: )  ); attr "IT" is  :::"Moufangian":::  means :: PAPDESAF:def 4 (Bool (Set   ($#k2_diraf :::"Lambda"::: )  "IT") "is"   ($#v7_aff_2 :::"Moufangian"::: )  ); attr "IT" is  :::"translation":::  means :: PAPDESAF:def 5 (Bool (Set   ($#k2_diraf :::"Lambda"::: )  "IT") "is"   ($#v11_aff_2 :::"translational"::: )  ); end; 
















:: deftheorem    defines :::"Pappian"::: PAPDESAF:def 2 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_papdesaf :::"Pappian"::: )  ) "iff" (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "IT"))) "is"   ($#v2_aff_2 :::"Pappian"::: )  )  ")" )); 
 
:: deftheorem    defines :::"Desarguesian"::: PAPDESAF:def 3 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_papdesaf :::"Desarguesian"::: )  ) "iff" (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "IT"))) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )  ")" )); 
 
:: deftheorem    defines :::"Moufangian"::: PAPDESAF:def 4 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_papdesaf :::"Moufangian"::: )  ) "iff" (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "IT"))) "is"   ($#v7_aff_2 :::"Moufangian"::: )  )  ")" )); 
 
:: deftheorem    defines :::"translation"::: PAPDESAF:def 5 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_papdesaf :::"translation"::: )  ) "iff" (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "IT"))) "is"   ($#v11_aff_2 :::"translational"::: )  )  ")" )); 
 definitionlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); attr "OAS" is  :::"satisfying_DES":::  means :: PAPDESAF:def 6 (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS"  "st" (Bool (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a1")) "," (Set (Var "c1")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "c1")))); end; 




:: deftheorem    defines :::"satisfying_DES"::: PAPDESAF:def 6 :  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "OAS")) "is"   ($#v5_papdesaf :::"satisfying_DES"::: )  ) "iff" (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a1")) "," (Set (Var "c1")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "c1"))))  ")" )); 
 definitionlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); attr "OAS" is  :::"satisfying_DES_1":::  means :: PAPDESAF:def 7 (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS"  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "o"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "b")) "," (Set (Var "o"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "c")) "," (Set (Var "o"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "a1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c1")) "," (Set (Var "a1")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c1")) "," (Set (Var "b1")))); end; 




:: deftheorem    defines :::"satisfying_DES_1"::: PAPDESAF:def 7 :  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "OAS")) "is"   ($#v6_papdesaf :::"satisfying_DES_1"::: )  ) "iff" (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "o"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "b")) "," (Set (Var "o"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "c")) "," (Set (Var "o"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "a1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c1")) "," (Set (Var "a1")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c1")) "," (Set (Var "b1"))))  ")" )); 
 
theorem :: PAPDESAF:6 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAS")) "is"   ($#v6_papdesaf :::"satisfying_DES_1"::: )  )) "holds"  (Bool (Set (Var "OAS")) "is"   ($#v5_papdesaf :::"satisfying_DES"::: )  )) ; 
 
theorem :: PAPDESAF:7 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Set (Var "a")) "," (Set (Var "o"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a9"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "a9")) "," (Set (Var "b9")))) "holds"  (Bool  "("  (Bool (Set (Var "b")) "," (Set (Var "o"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b9")) "," (Set (Var "a9")))  ")" ))) ; 
 
theorem :: PAPDESAF:8 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a9"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "a9")) "," (Set (Var "b9")))) "holds"  (Bool  "("  (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "b9")))  ")" ))) ; 
 
theorem :: PAPDESAF:9 (Bool  "for" (Set (Var "OAP")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAP")) "is"   ($#v6_papdesaf :::"satisfying_DES_1"::: )  )) "holds"  (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAP"))) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )) ; 
 
theorem :: PAPDESAF:10 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u1")) "," (Set (Var "v1")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Set (Var "o"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "u1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "o")) ")" ))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "o")) "," (Set (Var "v"))  ($#r1_geomtrap :::"'||'"::: )  (Set (Var "o")) "," (Set (Var "v1"))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "u"))  ($#r1_geomtrap :::"'||'"::: )  (Set (Var "o")) "," (Set (Var "v")))) & (Bool (Set (Var "u")) "," (Set (Var "v"))  ($#r1_geomtrap :::"'||'"::: )  (Set (Var "u1")) "," (Set (Var "v1")))) "holds"  (Bool  "("  (Bool (Set (Var "v1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "u1"))  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "r")) ")" )  ($#k2_real_1 :::"""::: )  ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "u")) ")" ) ")" ))) & (Bool (Set (Var "v1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o"))  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "r")) ")" )  ($#k2_real_1 :::"""::: )  ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "o")) ")" ) ")" ))) & (Bool (Set (Set (Var "v"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set (Var "r")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "v1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "u1")) ")" )))  ")" )))) ; 
 
theorem :: PAPDESAF:11 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analoaf :::"OASpace"::: )  (Set (Var "V"))))) "holds"  (Bool (Set (Var "OAS")) "is"   ($#v6_papdesaf :::"satisfying_DES_1"::: )  ))) ; 
 
theorem :: PAPDESAF:12 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analoaf :::"OASpace"::: )  (Set (Var "V"))))) "holds"  (Bool  "("  (Bool (Set (Var "OAS")) "is"   ($#v6_papdesaf :::"satisfying_DES_1"::: )  ) & (Bool (Set (Var "OAS")) "is"   ($#v5_papdesaf :::"satisfying_DES"::: )  )  ")" ))) ; 
 
theorem :: PAPDESAF:13 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analoaf :::"OASpace"::: )  (Set (Var "V"))))) "holds"  (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS"))) "is"   ($#v2_aff_2 :::"Pappian"::: )  ))) ; 
 
theorem :: PAPDESAF:14 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analoaf :::"OASpace"::: )  (Set (Var "V"))))) "holds"  (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS"))) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  ))) ; 
 
theorem :: PAPDESAF:15 (Bool  "for" (Set (Var "AS")) "being"   ($#l1_analoaf :::"AffinSpace":::)  "st" (Bool (Bool (Set (Var "AS")) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )) "holds"  (Bool (Set (Var "AS")) "is"   ($#v7_aff_2 :::"Moufangian"::: )  )) ; 
 
theorem :: PAPDESAF:16 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analoaf :::"OASpace"::: )  (Set (Var "V"))))) "holds"  (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS"))) "is"   ($#v7_aff_2 :::"Moufangian"::: )  ))) ; 
 
theorem :: PAPDESAF:17 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  "st" (Bool (Bool (Set (Var "OAS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analoaf :::"OASpace"::: )  (Set (Var "V"))))) "holds"  (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS"))) "is"   ($#v11_aff_2 :::"translational"::: )  ))) ; 
 
theorem :: PAPDESAF:18 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"  (Bool (Set   ($#k2_diraf :::"Lambda"::: )  (Set (Var "OAS"))) "is"   ($#v1_translac :::"Fanoian"::: )  )) ; 
 registration
cluster bbbadV2_STRUCT_0()  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v2_analoaf :::"OAffinSpace-like"::: )     ($#v1_papdesaf :::"Pappian"::: )     ($#v2_papdesaf :::"Desarguesian"::: )     ($#v3_papdesaf :::"Moufangian"::: )     ($#v4_papdesaf :::"translation"::: )    for    ($#l1_analoaf :::"AffinStruct"::: )  ; 
end; registration
cluster bbbadV2_STRUCT_0()  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v1_analoaf :::"strict"::: )     ($#v1_diraf :::"AffinSpace-like"::: )     ($#v2_diraf :::"2-dimensional"::: )     ($#v2_aff_2 :::"Pappian"::: )     ($#v4_aff_2 :::"Desarguesian"::: )     ($#v7_aff_2 :::"Moufangian"::: )     ($#v11_aff_2 :::"translational"::: )     ($#v1_translac :::"Fanoian"::: )    for    ($#l1_analoaf :::"AffinStruct"::: )  ; 
end; registration
cluster bbbadV2_STRUCT_0()  ($#~v7_struct_0  "non"   ($#v7_struct_0 :::"trivial"::: )   )    ($#v1_analoaf :::"strict"::: )     ($#v1_diraf :::"AffinSpace-like"::: )     ($#v2_aff_2 :::"Pappian"::: )     ($#v4_aff_2 :::"Desarguesian"::: )     ($#v7_aff_2 :::"Moufangian"::: )     ($#v11_aff_2 :::"translational"::: )     ($#v1_translac :::"Fanoian"::: )    for    ($#l1_analoaf :::"AffinStruct"::: )  ; 
end; registrationlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); 
cluster (Set   ($#k2_diraf :::"Lambda"::: )  "OAS") ->   ($#v1_translac :::"Fanoian"::: )   ; 
end; registrationlet "OAS" be   ($#v1_papdesaf :::"Pappian"::: )    ($#l1_analoaf :::"OAffinSpace":::); 
cluster (Set   ($#k2_diraf :::"Lambda"::: )  "OAS") ->   ($#v2_aff_2 :::"Pappian"::: )   ; 
end; registrationlet "OAS" be   ($#v2_papdesaf :::"Desarguesian"::: )    ($#l1_analoaf :::"OAffinSpace":::); 
cluster (Set   ($#k2_diraf :::"Lambda"::: )  "OAS") ->   ($#v4_aff_2 :::"Desarguesian"::: )   ; 
end; registrationlet "OAS" be   ($#v3_papdesaf :::"Moufangian"::: )    ($#l1_analoaf :::"OAffinSpace":::); 
cluster (Set   ($#k2_diraf :::"Lambda"::: )  "OAS") ->   ($#v7_aff_2 :::"Moufangian"::: )   ; 
end; registrationlet "OAS" be   ($#v4_papdesaf :::"translation"::: )    ($#l1_analoaf :::"OAffinSpace":::); 
cluster (Set   ($#k2_diraf :::"Lambda"::: )  "OAS") ->   ($#v11_aff_2 :::"translational"::: )   ; 
end;