:: AFF_2 semantic presentation begin definitionlet "AP" be ($#l1_analoaf :::"AffinPlane":::); attr "AP" is :::"satisfying_PPAP"::: means :: AFF_2:def 1 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" "AP" "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 "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (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")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))))); end; :: deftheorem defines :::"satisfying_PPAP"::: AFF_2:def 1 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v1_aff_2 :::"satisfying_PPAP"::: ) ) "iff" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (Bool "for" (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 "AP")) "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 "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (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")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinSpace":::); attr "AP" is :::"Pappian"::: means :: AFF_2:def 2 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (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" "AP" "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 "a"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a9"))) & (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 "c"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (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")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))))); end; :: deftheorem defines :::"Pappian"::: AFF_2:def 2 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v2_aff_2 :::"Pappian"::: ) ) "iff" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (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 "AP")) "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 "a"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a9"))) & (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 "c"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (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")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinPlane":::); attr "AP" is :::"satisfying_PAP_1"::: means :: AFF_2:def 3 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (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" "AP" "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 "a"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a9"))) & (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 "c"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (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 (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))))); end; :: deftheorem defines :::"satisfying_PAP_1"::: AFF_2:def 3 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v3_aff_2 :::"satisfying_PAP_1"::: ) ) "iff" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (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 "AP")) "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 "a"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "a9"))) & (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 "c"))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (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 (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinSpace":::); attr "AP" is :::"Desarguesian"::: means :: AFF_2:def 4 (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (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" "AP" "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 "a9")) ($#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")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))))); end; :: deftheorem defines :::"Desarguesian"::: AFF_2:def 4 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v4_aff_2 :::"Desarguesian"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (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 "AP")) "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 "a9")) ($#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")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinPlane":::); attr "AP" is :::"satisfying_DES_1"::: means :: AFF_2:def 5 (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (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" "AP" "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")) ($#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 "a9")) ($#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 (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9")))) "holds" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))))); end; :: deftheorem defines :::"satisfying_DES_1"::: AFF_2:def 5 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v5_aff_2 :::"satisfying_DES_1"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (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 "AP")) "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")) ($#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 "a9")) ($#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 (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9")))) "holds" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinPlane":::); attr "AP" is :::"satisfying_DES_2"::: means :: AFF_2:def 6 (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (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" "AP" "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 "a9")) ($#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 "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 (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))))); end; :: deftheorem defines :::"satisfying_DES_2"::: AFF_2:def 6 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v6_aff_2 :::"satisfying_DES_2"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (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 "AP")) "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 "a9")) ($#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 "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 (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9")))) "holds" (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinSpace":::); attr "AP" is :::"Moufangian"::: means :: AFF_2:def 7 (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (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" "AP" "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (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 (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))))); end; :: deftheorem defines :::"Moufangian"::: AFF_2:def 7 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v7_aff_2 :::"Moufangian"::: ) ) "iff" (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (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 "AP")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (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 (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinPlane":::); attr "AP" is :::"satisfying_TDES_1"::: means :: AFF_2:def 8 (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (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" "AP" "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K")))) "holds" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))))); end; :: deftheorem defines :::"satisfying_TDES_1"::: AFF_2:def 8 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v8_aff_2 :::"satisfying_TDES_1"::: ) ) "iff" (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (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 "AP")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K")))) "holds" (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinPlane":::); attr "AP" is :::"satisfying_TDES_2"::: means :: AFF_2:def 9 (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (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" "AP" "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))))); end; :: deftheorem defines :::"satisfying_TDES_2"::: AFF_2:def 9 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v9_aff_2 :::"satisfying_TDES_2"::: ) ) "iff" (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (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 "AP")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_analoaf :::"//"::: ) (Set (Var "a9")) "," (Set (Var "b9"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinPlane":::); attr "AP" is :::"satisfying_TDES_3"::: means :: AFF_2:def 10 (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (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" "AP" "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (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 (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))))); end; :: deftheorem defines :::"satisfying_TDES_3"::: AFF_2:def 10 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v10_aff_2 :::"satisfying_TDES_3"::: ) ) "iff" (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (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 "AP")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v1_aff_1 :::"being_line"::: ) ) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) & (Bool (Set (Var "o")) ($#r1_hidden :::"<>"::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9"))) & (Bool ($#r1_aff_1 :::"LIN"::: ) (Set (Var "o")) "," (Set (Var "b")) "," (Set (Var "b9"))) & (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 (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_aff_1 :::"//"::: ) (Set (Var "K")))) "holds" (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinSpace":::); attr "AP" is :::"translational"::: means :: AFF_2:def 11 (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" "AP" "st" (Bool (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P"))) & (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a9")) ($#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")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))))); end; :: deftheorem defines :::"translational"::: AFF_2:def 11 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v11_aff_2 :::"translational"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (Bool "for" (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 "AP")) "st" (Bool (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P"))) & (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a9")) ($#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")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinPlane":::); attr "AP" is :::"satisfying_des_1"::: means :: AFF_2:def 12 (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" "AP" "st" (Bool (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a9")) ($#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 (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9")))) "holds" (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))))); end; :: deftheorem defines :::"satisfying_des_1"::: AFF_2:def 12 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v12_aff_2 :::"satisfying_des_1"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "P")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (Bool "for" (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 "AP")) "st" (Bool (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "P"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a9")) ($#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 (Set (Var "b")) "," (Set (Var "c")) ($#r2_analoaf :::"//"::: ) (Set (Var "b9")) "," (Set (Var "c9"))) & (Bool (Bool "not" ($#r1_aff_1 :::"LIN"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "c9")))) "holds" (Bool (Set (Var "A")) ($#r5_aff_1 :::"//"::: ) (Set (Var "C"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinSpace":::); attr "AP" is :::"satisfying_pap"::: means :: AFF_2:def 13 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" "AP" "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 "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (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")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))))); end; :: deftheorem defines :::"satisfying_pap"::: AFF_2:def 13 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinSpace":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v13_aff_2 :::"satisfying_pap"::: ) ) "iff" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (Bool "for" (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 "AP")) "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 "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (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")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))))) ")" )); definitionlet "AP" be ($#l1_analoaf :::"AffinPlane":::); attr "AP" is :::"satisfying_pap_1"::: means :: AFF_2:def 14 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "AP" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element":::) "of" "AP" "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 "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b9")) ($#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 (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))) & (Bool (Set (Var "a9")) ($#r1_hidden :::"<>"::: ) (Set (Var "b9")))) "holds" (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))))); end; :: deftheorem defines :::"satisfying_pap_1"::: AFF_2:def 14 : (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v14_aff_2 :::"satisfying_pap_1"::: ) ) "iff" (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "AP")) (Bool "for" (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 "AP")) "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 "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) ($#r5_aff_1 :::"//"::: ) (Set (Var "N"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"<>"::: ) (Set (Var "N"))) & (Bool (Set (Var "a9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Var "b9")) ($#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 (Set (Var "a")) "," (Set (Var "c9")) ($#r2_analoaf :::"//"::: ) (Set (Var "c")) "," (Set (Var "a9"))) & (Bool (Set (Var "a9")) ($#r1_hidden :::"<>"::: ) (Set (Var "b9")))) "holds" (Bool (Set (Var "c9")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))))) ")" )); theorem :: AFF_2:1 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v2_aff_2 :::"Pappian"::: ) ) "iff" (Bool (Set (Var "AP")) "is" ($#v3_aff_2 :::"satisfying_PAP_1"::: ) ) ")" )) ; theorem :: AFF_2:2 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v4_aff_2 :::"Desarguesian"::: ) ) "iff" (Bool (Set (Var "AP")) "is" ($#v5_aff_2 :::"satisfying_DES_1"::: ) ) ")" )) ; theorem :: AFF_2:3 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v7_aff_2 :::"Moufangian"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v8_aff_2 :::"satisfying_TDES_1"::: ) )) ; theorem :: AFF_2:4 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v8_aff_2 :::"satisfying_TDES_1"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v9_aff_2 :::"satisfying_TDES_2"::: ) )) ; theorem :: AFF_2:5 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v9_aff_2 :::"satisfying_TDES_2"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v10_aff_2 :::"satisfying_TDES_3"::: ) )) ; theorem :: AFF_2:6 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v10_aff_2 :::"satisfying_TDES_3"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v7_aff_2 :::"Moufangian"::: ) )) ; theorem :: AFF_2:7 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v11_aff_2 :::"translational"::: ) ) "iff" (Bool (Set (Var "AP")) "is" ($#v12_aff_2 :::"satisfying_des_1"::: ) ) ")" )) ; theorem :: AFF_2:8 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v13_aff_2 :::"satisfying_pap"::: ) ) "iff" (Bool (Set (Var "AP")) "is" ($#v14_aff_2 :::"satisfying_pap_1"::: ) ) ")" )) ; theorem :: AFF_2:9 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v2_aff_2 :::"Pappian"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v13_aff_2 :::"satisfying_pap"::: ) )) ; theorem :: AFF_2:10 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "holds" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v1_aff_2 :::"satisfying_PPAP"::: ) ) "iff" (Bool "(" (Bool (Set (Var "AP")) "is" ($#v2_aff_2 :::"Pappian"::: ) ) & (Bool (Set (Var "AP")) "is" ($#v13_aff_2 :::"satisfying_pap"::: ) ) ")" ) ")" )) ; theorem :: AFF_2:11 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v2_aff_2 :::"Pappian"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v4_aff_2 :::"Desarguesian"::: ) )) ; theorem :: AFF_2:12 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v4_aff_2 :::"Desarguesian"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v7_aff_2 :::"Moufangian"::: ) )) ; theorem :: AFF_2:13 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v8_aff_2 :::"satisfying_TDES_1"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v12_aff_2 :::"satisfying_des_1"::: ) )) ; theorem :: AFF_2:14 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v7_aff_2 :::"Moufangian"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v11_aff_2 :::"translational"::: ) )) ; theorem :: AFF_2:15 (Bool "for" (Set (Var "AP")) "being" ($#l1_analoaf :::"AffinPlane":::) "st" (Bool (Bool (Set (Var "AP")) "is" ($#v11_aff_2 :::"translational"::: ) )) "holds" (Bool (Set (Var "AP")) "is" ($#v13_aff_2 :::"satisfying_pap"::: ) )) ;