:: EUCLMETR  semantic presentation begin  definitionlet "IT" be   ($#l1_analmetr :::"OrtAfSp":::); attr "IT" is  :::"Euclidean":::  means :: EUCLMETR:def 1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "d"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "c")))); end; 




:: deftheorem    defines :::"Euclidean"::: EUCLMETR:def 1 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analmetr :::"OrtAfSp":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_euclmetr :::"Euclidean"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "d")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "d"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "c"))))  ")" )); 
 definitionlet "IT" be   ($#l1_analmetr :::"OrtAfSp":::); attr "IT" is  :::"Pappian":::  means :: EUCLMETR:def 2 (Bool (Set   ($#k3_analmetr :::"Af"::: )  "IT") "is"   ($#v2_aff_2 :::"Pappian"::: )  ); end; 




:: deftheorem    defines :::"Pappian"::: EUCLMETR:def 2 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analmetr :::"OrtAfSp":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_euclmetr :::"Pappian"::: )  ) "iff" (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "IT"))) "is"   ($#v2_aff_2 :::"Pappian"::: )  )  ")" )); 
 definitionlet "IT" be   ($#l1_analmetr :::"OrtAfSp":::); attr "IT" is  :::"Desarguesian":::  means :: EUCLMETR:def 3 (Bool (Set   ($#k3_analmetr :::"Af"::: )  "IT") "is"   ($#v4_aff_2 :::"Desarguesian"::: )  ); end; 




:: deftheorem    defines :::"Desarguesian"::: EUCLMETR:def 3 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analmetr :::"OrtAfSp":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_euclmetr :::"Desarguesian"::: )  ) "iff" (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "IT"))) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )  ")" )); 
 definitionlet "IT" be   ($#l1_analmetr :::"OrtAfSp":::); attr "IT" is  :::"Fanoian":::  means :: EUCLMETR:def 4 (Bool (Set   ($#k3_analmetr :::"Af"::: )  "IT") "is"   ($#v1_translac :::"Fanoian"::: )  ); end; 




:: deftheorem    defines :::"Fanoian"::: EUCLMETR:def 4 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analmetr :::"OrtAfSp":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_euclmetr :::"Fanoian"::: )  ) "iff" (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "IT"))) "is"   ($#v1_translac :::"Fanoian"::: )  )  ")" )); 
 definitionlet "IT" be   ($#l1_analmetr :::"OrtAfSp":::); attr "IT" is  :::"Moufangian":::  means :: EUCLMETR:def 5 (Bool (Set   ($#k3_analmetr :::"Af"::: )  "IT") "is"   ($#v7_aff_2 :::"Moufangian"::: )  ); end; 




:: deftheorem    defines :::"Moufangian"::: EUCLMETR:def 5 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analmetr :::"OrtAfSp":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v5_euclmetr :::"Moufangian"::: )  ) "iff" (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "IT"))) "is"   ($#v7_aff_2 :::"Moufangian"::: )  )  ")" )); 
 definitionlet "IT" be   ($#l1_analmetr :::"OrtAfSp":::); attr "IT" is  :::"translation":::  means :: EUCLMETR:def 6 (Bool (Set   ($#k3_analmetr :::"Af"::: )  "IT") "is"   ($#v11_aff_2 :::"translational"::: )  ); end; 




:: deftheorem    defines :::"translation"::: EUCLMETR:def 6 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analmetr :::"OrtAfSp":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v6_euclmetr :::"translation"::: )  ) "iff" (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "IT"))) "is"   ($#v11_aff_2 :::"translational"::: )  )  ")" )); 
 definitionlet "IT" be   ($#l1_analmetr :::"OrtAfSp":::); attr "IT" is  :::"Homogeneous":::  means :: EUCLMETR:def 7 (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")) "," (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  "st" (Bool (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a")))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b"))))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1")))); end; 




:: deftheorem    defines :::"Homogeneous"::: EUCLMETR:def 7 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_analmetr :::"OrtAfSp":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v7_euclmetr :::"Homogeneous"::: )  ) "iff" (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")) "," (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a")))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b"))))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1"))))  ")" )); 
 






theorem :: EUCLMETR:1 (Bool  "for" (Set (Var "MP")) "being"   ($#l1_analmetr :::"OrtAfSp":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MP"))  "st" (Bool (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))  ")" ))) ; 
 
theorem :: EUCLMETR:2 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS"))  (Bool  "for" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "MS")))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r6_analmetr :::"_|_"::: )  (Set (Var "K"))) & (Bool (Set (Var "c")) "," (Set (Var "d"))  ($#r6_analmetr :::"_|_"::: )  (Set (Var "K")))) "holds"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "d")) "," (Set (Var "c")))  ")" )))) ; 
 
theorem :: EUCLMETR:3 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "K")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "MS")))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r6_analmetr :::"_|_"::: )  (Set (Var "K"))) "or" (Bool (Set (Var "b")) "," (Set (Var "a"))  ($#r6_analmetr :::"_|_"::: )  (Set (Var "K")))  ")" ) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r6_analmetr :::"_|_"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "K"))  ($#r9_analmetr :::"//"::: )  (Set (Var "A")))))) ; 
 
theorem :: EUCLMETR:4 (Bool  "for" (Set (Var "MP")) "being"   ($#l1_analmetr :::"OrtAfSp":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MP"))  "st" (Bool (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")))) "holds"  (Bool  "("  (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "z"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")))  ")" ))) ; 
 
theorem :: EUCLMETR:5 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS"))  "st" (Bool (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS")) "st"  (Bool  "("  (Bool (Set (Var "d")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "d")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "c")))  ")" )))) ; 
 
theorem :: EUCLMETR:6 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS"))  "st" (Bool (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Set (Var "d1")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "d1")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "c"))) & (Bool (Set (Var "d2")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "d2")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "c")))) "holds"  (Bool (Set (Var "d1"))  ($#r1_hidden :::"="::: )  (Set (Var "d2"))))) ; 
 
theorem :: EUCLMETR:7 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a")) "," (Set (Var "d"))) & (Bool   ($#r5_analmetr :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))))) ; 
 
theorem :: EUCLMETR:8 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "MS")) "is"   ($#v1_euclmetr :::"Euclidean"::: )  ) "iff" (Bool (Set (Var "MS")) "is"   ($#v3_conaffm :::"satisfying_3H"::: )  )  ")" )) ; 
 
theorem :: EUCLMETR:9 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "MS")) "is"   ($#v7_euclmetr :::"Homogeneous"::: )  ) "iff" (Bool (Set (Var "MS")) "is"   ($#v4_conaffm :::"satisfying_ODES"::: )  )  ")" )) ; 
 
theorem :: EUCLMETR:10 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "MS")) "is"   ($#v2_euclmetr :::"Pappian"::: )  ) "iff" (Bool (Set (Var "MS")) "is"   ($#v2_conmetr :::"satisfying_PAP"::: )  )  ")" )) ; 
 
theorem :: EUCLMETR:11 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "MS")) "is"   ($#v3_euclmetr :::"Desarguesian"::: )  ) "iff" (Bool (Set (Var "MS")) "is"   ($#v1_conaffm :::"satisfying_DES"::: )  )  ")" )) ; 
 
theorem :: EUCLMETR:12 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "MS")) "is"   ($#v5_euclmetr :::"Moufangian"::: )  ) "iff" (Bool (Set (Var "MS")) "is"   ($#v5_conmetr :::"satisfying_TDES"::: )  )  ")" )) ; 
 
theorem :: EUCLMETR:13 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "MS")) "is"   ($#v6_euclmetr :::"translation"::: )  ) "iff" (Bool (Set (Var "MS")) "is"   ($#v8_conmetr :::"satisfying_des"::: )  )  ")" )) ; 
 
theorem :: EUCLMETR:14 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  "st" (Bool (Bool (Set (Var "MS")) "is"   ($#v7_euclmetr :::"Homogeneous"::: )  )) "holds"  (Bool (Set (Var "MS")) "is"   ($#v3_euclmetr :::"Desarguesian"::: )  )) ; 
 
theorem :: EUCLMETR:15 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  "st" (Bool (Bool (Set (Var "MS")) "is"   ($#v1_euclmetr :::"Euclidean"::: )  ) & (Bool (Set (Var "MS")) "is"   ($#v3_euclmetr :::"Desarguesian"::: )  )) "holds"  (Bool (Set (Var "MS")) "is"   ($#v2_euclmetr :::"Pappian"::: )  )) ; 
 









theorem :: EUCLMETR:16 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "c1")) "," (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS"))  "st" (Bool (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "a")))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a2"))) & (Bool (Set (Var "c")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "c1")) "," (Set (Var "a1"))) & (Bool (Set (Var "c")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "c1")) "," (Set (Var "a2")))) "holds"  (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set (Var "a2"))))) ; 
 
theorem :: EUCLMETR:17 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "c1")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS"))  "st" (Bool (Bool (Bool  "not"   ($#r5_analmetr :::"LIN"::: )  (Set (Var "o")) "," (Set (Var "c")) "," (Set (Var "a"))))) "holds"  (Bool  "ex" (Set (Var "a1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS")) "st"  (Bool  "("  (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "a1"))) & (Bool (Set (Var "c")) "," (Set (Var "a"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "c1")) "," (Set (Var "a1")))  ")" )))) ; 
 
theorem :: EUCLMETR:18 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool   ($#r1_analmetr :::"Gen"::: )  (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))  ($#r1_hidden :::"<>"::: )  (Set (Var "u"))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))  ($#r1_hidden :::"<>"::: )  (Set (Var "v"))) & (Bool (Set (Var "u")) "," (Set (Var "v"))  ($#r2_analmetr :::"are_Ort_wrt"::: )  (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "w")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "y")) ")" )))) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "c"))  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "w")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "y")) ")" )))  ")" ))))) ; 
 
theorem :: EUCLMETR:19 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "w")) "," (Set (Var "y")) "," (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool   ($#r1_analmetr :::"Gen"::: )  (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))  ($#r1_hidden :::"<>"::: )  (Set (Var "u"))) & (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "V")))  ($#r1_hidden :::"<>"::: )  (Set (Var "v"))) & (Bool (Set (Var "u")) "," (Set (Var "v"))  ($#r2_analmetr :::"are_Ort_wrt"::: )  (Set (Var "w")) "," (Set (Var "y")))) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "w")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "y")) ")" )) "," (Set (Set  "(" (Set  "(" (Set (Var "c"))  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "w")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r2_analmetr :::"are_Ort_wrt"::: )  (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "w")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "u"))) "," (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "c"))  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "w")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "y")) ")" ) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "v")))  ($#r2_analmetr :::"are_Ort_wrt"::: )  (Set (Var "w")) "," (Set (Var "y")))  ")" ))))) ; 
 
theorem :: EUCLMETR:20 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "w")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool   ($#r1_analmetr :::"Gen"::: )  (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "MS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analmetr :::"AMSpace"::: )   "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ))) "holds"  (Bool (Set (Var "MS")) "is"   ($#v5_conaffm :::"satisfying_LIN"::: )  )))) ; 
 
theorem :: EUCLMETR:21 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a1")) "," (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "c")) "," (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "MS"))  "st" (Bool (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "b1"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "o")) "," (Set (Var "c1"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "b1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "a1")) "," (Set (Var "c1"))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a")))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b")))) & (Bool (Set (Var "o"))  ($#r1_hidden :::"="::: )  (Set (Var "a1")))) "holds"  (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r4_analmetr :::"_|_"::: )  (Set (Var "b1")) "," (Set (Var "c1"))))) ; 
 
theorem :: EUCLMETR:22 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "w")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool   ($#r1_analmetr :::"Gen"::: )  (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "MS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analmetr :::"AMSpace"::: )   "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ))) "holds"  (Bool (Set (Var "MS")) "is"   ($#v7_euclmetr :::"Homogeneous"::: )  )))) ; 
 registration
cluster bbbadV2_STRUCT_0()   ($#v2_analmetr :::"OrtAfSp-like"::: )     ($#v3_analmetr :::"OrtAfPl-like"::: )     ($#v1_euclmetr :::"Euclidean"::: )     ($#v2_euclmetr :::"Pappian"::: )     ($#v3_euclmetr :::"Desarguesian"::: )     ($#v4_euclmetr :::"Fanoian"::: )     ($#v5_euclmetr :::"Moufangian"::: )     ($#v6_euclmetr :::"translation"::: )     ($#v7_euclmetr :::"Homogeneous"::: )    for    ($#l1_analmetr :::"ParOrtStr"::: )  ; 
end; registration
cluster bbbadV2_STRUCT_0()   ($#v2_analmetr :::"OrtAfSp-like"::: )     ($#v1_euclmetr :::"Euclidean"::: )     ($#v2_euclmetr :::"Pappian"::: )     ($#v3_euclmetr :::"Desarguesian"::: )     ($#v4_euclmetr :::"Fanoian"::: )     ($#v5_euclmetr :::"Moufangian"::: )     ($#v6_euclmetr :::"translation"::: )     ($#v7_euclmetr :::"Homogeneous"::: )    for    ($#l1_analmetr :::"ParOrtStr"::: )  ; 
end; 
theorem :: EUCLMETR:23 (Bool  "for" (Set (Var "MS")) "being"   ($#l1_analmetr :::"OrtAfPl":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "w")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool   ($#r1_analmetr :::"Gen"::: )  (Set (Var "w")) "," (Set (Var "y"))) & (Bool (Set (Var "MS"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_analmetr :::"AMSpace"::: )   "(" (Set (Var "V")) "," (Set (Var "w")) "," (Set (Var "y")) ")" ))) "holds"  (Bool (Set (Var "MS")) "is"   ($#v1_euclmetr :::"Euclidean"::: )     ($#v2_euclmetr :::"Pappian"::: )     ($#v3_euclmetr :::"Desarguesian"::: )     ($#v4_euclmetr :::"Fanoian"::: )     ($#v5_euclmetr :::"Moufangian"::: )     ($#v6_euclmetr :::"translation"::: )     ($#v7_euclmetr :::"Homogeneous"::: )    ($#l1_analmetr :::"OrtAfPl":::))))) ; 
 registrationlet "MS" be   ($#v2_euclmetr :::"Pappian"::: )    ($#l1_analmetr :::"OrtAfPl":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v2_aff_2 :::"Pappian"::: )   ; 
end; registrationlet "MS" be   ($#v3_euclmetr :::"Desarguesian"::: )    ($#l1_analmetr :::"OrtAfPl":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v4_aff_2 :::"Desarguesian"::: )   ; 
end; registrationlet "MS" be   ($#v5_euclmetr :::"Moufangian"::: )    ($#l1_analmetr :::"OrtAfPl":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v7_aff_2 :::"Moufangian"::: )   ; 
end; registrationlet "MS" be   ($#v6_euclmetr :::"translation"::: )    ($#l1_analmetr :::"OrtAfPl":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v11_aff_2 :::"translational"::: )   ; 
end; registrationlet "MS" be   ($#v4_euclmetr :::"Fanoian"::: )    ($#l1_analmetr :::"OrtAfPl":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v1_translac :::"Fanoian"::: )   ; 
end; registrationlet "MS" be   ($#v7_euclmetr :::"Homogeneous"::: )    ($#l1_analmetr :::"OrtAfPl":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v4_aff_2 :::"Desarguesian"::: )   ; 
end; registrationlet "MS" be   ($#v1_euclmetr :::"Euclidean"::: )     ($#v3_euclmetr :::"Desarguesian"::: )    ($#l1_analmetr :::"OrtAfPl":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v2_aff_2 :::"Pappian"::: )   ; 
end; registrationlet "MS" be   ($#v2_euclmetr :::"Pappian"::: )    ($#l1_analmetr :::"OrtAfSp":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v2_aff_2 :::"Pappian"::: )   ; 
end; registrationlet "MS" be   ($#v3_euclmetr :::"Desarguesian"::: )    ($#l1_analmetr :::"OrtAfSp":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v4_aff_2 :::"Desarguesian"::: )   ; 
end; registrationlet "MS" be   ($#v5_euclmetr :::"Moufangian"::: )    ($#l1_analmetr :::"OrtAfSp":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v7_aff_2 :::"Moufangian"::: )   ; 
end; registrationlet "MS" be   ($#v6_euclmetr :::"translation"::: )    ($#l1_analmetr :::"OrtAfSp":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v11_aff_2 :::"translational"::: )   ; 
end; registrationlet "MS" be   ($#v4_euclmetr :::"Fanoian"::: )    ($#l1_analmetr :::"OrtAfSp":::); 
cluster (Set   ($#k3_analmetr :::"Af"::: )  "MS") ->   ($#v1_translac :::"Fanoian"::: )   ; 
end;