:: CONMETR1  semantic presentation begin  






































definitionlet "X" be   ($#l1_analoaf :::"AffinPlane":::); attr "X" is  :::"satisfying_minor_Scherungssatz":::  means :: CONMETR1:def 1 (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X"  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "M"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "N"))) & (Bool (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4"))))); end; 




:: deftheorem    defines :::"satisfying_minor_Scherungssatz"::: CONMETR1:def 1 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_conmetr1 :::"satisfying_minor_Scherungssatz"::: )  ) "iff" (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "M"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "N"))) & (Bool (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4")))))  ")" )); 
 definitionlet "X" be   ($#l1_analoaf :::"AffinPlane":::); attr "X" is  :::"satisfying_major_Scherungssatz":::  means :: CONMETR1:def 2 (Bool  "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X"  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "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 "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4"))))); end; 




:: deftheorem    defines :::"satisfying_major_Scherungssatz"::: CONMETR1:def 2 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_conmetr1 :::"satisfying_major_Scherungssatz"::: )  ) "iff" (Bool  "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "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 "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4")))))  ")" )); 
 definitionlet "X" be   ($#l1_analoaf :::"AffinPlane":::); attr "X" is  :::"satisfying_Scherungssatz":::  means :: CONMETR1:def 3 (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X"  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "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 "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4"))))); end; 




:: deftheorem    defines :::"satisfying_Scherungssatz"::: CONMETR1:def 3 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_conmetr1 :::"satisfying_Scherungssatz"::: )  ) "iff" (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "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 "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4")))))  ")" )); 
 definitionlet "X" be   ($#l1_analoaf :::"AffinPlane":::); attr "X" is  :::"satisfying_indirect_Scherungssatz":::  means :: CONMETR1:def 4 (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X"  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "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 "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4"))))); end; 




:: deftheorem    defines :::"satisfying_indirect_Scherungssatz"::: CONMETR1:def 4 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_conmetr1 :::"satisfying_indirect_Scherungssatz"::: )  ) "iff" (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "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 "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4")))))  ")" )); 
 definitionlet "X" be   ($#l1_analoaf :::"AffinPlane":::); attr "X" is  :::"satisfying_minor_indirect_Scherungssatz":::  means :: CONMETR1:def 5 (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X"  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "M"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "N"))) & (Bool (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4"))))); end; 




:: deftheorem    defines :::"satisfying_minor_indirect_Scherungssatz"::: CONMETR1:def 5 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v5_conmetr1 :::"satisfying_minor_indirect_Scherungssatz"::: )  ) "iff" (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "M"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "N"))) & (Bool (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4")))))  ")" )); 
 definitionlet "X" be   ($#l1_analoaf :::"AffinPlane":::); attr "X" is  :::"satisfying_major_indirect_Scherungssatz":::  means :: CONMETR1:def 6 (Bool  "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X"  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "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 "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4"))))); end; 




:: deftheorem    defines :::"satisfying_major_indirect_Scherungssatz"::: CONMETR1:def 6 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v6_conmetr1 :::"satisfying_major_indirect_Scherungssatz"::: )  ) "iff" (Bool  "for" (Set (Var "o")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "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 "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Bool  "not" (Set (Var "a4"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) & (Bool (Bool  "not" (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "a3"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "b4"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Set (Var "a3")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b2"))) & (Bool (Set (Var "a2")) "," (Set (Var "a1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a1")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b4")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "a4"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b3")) "," (Set (Var "b4")))))  ")" )); 
 
theorem :: CONMETR1:1 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_conmetr1 :::"satisfying_indirect_Scherungssatz"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v5_conmetr1 :::"satisfying_minor_indirect_Scherungssatz"::: )  ) & (Bool (Set (Var "X")) "is"   ($#v6_conmetr1 :::"satisfying_major_indirect_Scherungssatz"::: )  )  ")" )  ")" )) ; 
 
theorem :: CONMETR1:2 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_conmetr1 :::"satisfying_Scherungssatz"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_conmetr1 :::"satisfying_minor_Scherungssatz"::: )  ) & (Bool (Set (Var "X")) "is"   ($#v2_conmetr1 :::"satisfying_major_Scherungssatz"::: )  )  ")" )  ")" )) ; 
 
theorem :: CONMETR1:3 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v5_conmetr1 :::"satisfying_minor_indirect_Scherungssatz"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_conmetr1 :::"satisfying_minor_Scherungssatz"::: )  )) ; 
 
theorem :: CONMETR1:4 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v6_conmetr1 :::"satisfying_major_indirect_Scherungssatz"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v2_conmetr1 :::"satisfying_major_Scherungssatz"::: )  )) ; 
 
theorem :: CONMETR1:5 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_conmetr1 :::"satisfying_indirect_Scherungssatz"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v3_conmetr1 :::"satisfying_Scherungssatz"::: )  )) ; 
 
theorem :: CONMETR1:6 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v11_aff_2 :::"translational"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_conmetr1 :::"satisfying_minor_Scherungssatz"::: )  )) ; 
 
theorem :: CONMETR1:7 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v2_conmetr1 :::"satisfying_major_Scherungssatz"::: )  )) ; 
 
theorem :: CONMETR1:8 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  ) "iff" (Bool (Set (Var "X")) "is"   ($#v3_conmetr1 :::"satisfying_Scherungssatz"::: )  )  ")" )) ; 
 
theorem :: CONMETR1:9 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v13_aff_2 :::"satisfying_pap"::: )  ) "iff" (Bool (Set (Var "X")) "is"   ($#v5_conmetr1 :::"satisfying_minor_indirect_Scherungssatz"::: )  )  ")" )) ; 
 
theorem :: CONMETR1:10 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_aff_2 :::"Pappian"::: )  ) "iff" (Bool (Set (Var "X")) "is"   ($#v6_conmetr1 :::"satisfying_major_indirect_Scherungssatz"::: )  )  ")" )) ; 
 
theorem :: CONMETR1:11 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_aff_2 :::"satisfying_PPAP"::: )  ) "iff" (Bool (Set (Var "X")) "is"   ($#v4_conmetr1 :::"satisfying_indirect_Scherungssatz"::: )  )  ")" )) ; 
 
theorem :: CONMETR1:12 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v6_conmetr1 :::"satisfying_major_indirect_Scherungssatz"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v5_conmetr1 :::"satisfying_minor_indirect_Scherungssatz"::: )  )) ; 
 










































theorem :: CONMETR1:13 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "X"))) "is"   ($#v3_conmetr1 :::"satisfying_Scherungssatz"::: )  ) "iff" (Bool (Set (Var "X")) "is"   ($#v6_conmetr :::"satisfying_SCH"::: )  )  ")" )) ; 
 
theorem :: CONMETR1:14 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v5_conmetr :::"satisfying_TDES"::: )  ) "iff" (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "X"))) "is"   ($#v7_aff_2 :::"Moufangian"::: )  )  ")" )) ; 
 
theorem :: CONMETR1:15 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "X"))) "is"   ($#v11_aff_2 :::"translational"::: )  ) "iff" (Bool (Set (Var "X")) "is"   ($#v8_conmetr :::"satisfying_des"::: )  )  ")" )) ; 
 
theorem :: CONMETR1:16 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_conmetr :::"satisfying_PAP"::: )  ) "iff" (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "X"))) "is"   ($#v2_aff_2 :::"Pappian"::: )  )  ")" )) ; 
 
theorem :: CONMETR1:17 (Bool  "for" (Set (Var "X")) "being"   ($#l1_analmetr :::"OrtAfPl":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_conaffm :::"satisfying_DES"::: )  ) "iff" (Bool (Set   ($#k3_analmetr :::"Af"::: )  (Set (Var "X"))) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )  ")" )) ;