:: AFF_3  semantic presentation begin  
























definitionlet "AP" be   ($#l1_analoaf :::"AffinPlane":::); attr "AP" is  :::"satisfying_DES1":::  means :: AFF_3:def 1 (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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AP"  "st" (Bool (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 "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b9"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c9"))  ($#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 "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q"))))); end; 




:: deftheorem    defines :::"satisfying_DES1"::: AFF_3:def 1 :  (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v1_aff_3 :::"satisfying_DES1"::: )  ) "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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP"))  "st" (Bool (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 "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b9"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c9"))  ($#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 "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))))  ")" )); 
 definitionlet "AP" be   ($#l1_analoaf :::"AffinPlane":::); attr "AP" is  :::"satisfying_DES1_1":::  means :: AFF_3:def 2 (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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AP"  "st" (Bool (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 "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b9"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c9"))  ($#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 "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))))); end; 




:: deftheorem    defines :::"satisfying_DES1_1"::: AFF_3:def 2 :  (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v2_aff_3 :::"satisfying_DES1_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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP"))  "st" (Bool (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 "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "b9"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c9"))  ($#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 "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9")))))  ")" )); 
 definitionlet "AP" be   ($#l1_analoaf :::"AffinPlane":::); attr "AP" is  :::"satisfying_DES1_2":::  means :: AFF_3:def 3 (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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AP"  "st" (Bool (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 "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (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 "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 "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))))); end; 




:: deftheorem    defines :::"satisfying_DES1_2"::: AFF_3:def 3 :  (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v3_aff_3 :::"satisfying_DES1_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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP"))  "st" (Bool (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 "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "a9"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (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 "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 "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))))  ")" )); 
 definitionlet "AP" be   ($#l1_analoaf :::"AffinPlane":::); attr "AP" is  :::"satisfying_DES1_3":::  means :: AFF_3: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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AP"  "st" (Bool (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 "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (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 "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c9"))  ($#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 "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))))); end; 




:: deftheorem    defines :::"satisfying_DES1_3"::: AFF_3:def 4 :  (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v4_aff_3 :::"satisfying_DES1_3"::: )  ) "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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP"))  "st" (Bool (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 "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "C"))) & (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (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 "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "c9"))  ($#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 "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b9"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "o"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))))  ")" )); 
 definitionlet "AP" be   ($#l1_analoaf :::"AffinPlane":::); attr "AP" is  :::"satisfying_DES2":::  means :: AFF_3:def 5 (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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AP"  "st" (Bool (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 "P"))  ($#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"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "P"))) & (Bool (Set (Var "A"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "C"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q"))))); end; 




:: deftheorem    defines :::"satisfying_DES2"::: AFF_3:def 5 :  (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v5_aff_3 :::"satisfying_DES2"::: )  ) "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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP"))  "st" (Bool (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 "P"))  ($#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"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "P"))) & (Bool (Set (Var "A"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "C"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))))  ")" )); 
 definitionlet "AP" be   ($#l1_analoaf :::"AffinPlane":::); attr "AP" is  :::"satisfying_DES2_1":::  means :: AFF_3:def 6 (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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AP"  "st" (Bool (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 "P"))  ($#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"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "P"))) & (Bool (Set (Var "A"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "C"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))))); end; 




:: deftheorem    defines :::"satisfying_DES2_1"::: AFF_3:def 6 :  (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v6_aff_3 :::"satisfying_DES2_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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP"))  "st" (Bool (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 "P"))  ($#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"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "P"))) & (Bool (Set (Var "A"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "C"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9")))))  ")" )); 
 definitionlet "AP" be   ($#l1_analoaf :::"AffinPlane":::); attr "AP" is  :::"satisfying_DES2_2":::  means :: AFF_3:def 7 (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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AP"  "st" (Bool (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 "P"))  ($#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"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "C"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "A"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "P"))))); end; 




:: deftheorem    defines :::"satisfying_DES2_2"::: AFF_3:def 7 :  (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v7_aff_3 :::"satisfying_DES2_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 "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP"))  "st" (Bool (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 "P"))  ($#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"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "C"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "A"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "P")))))  ")" )); 
 definitionlet "AP" be   ($#l1_analoaf :::"AffinPlane":::); attr "AP" is  :::"satisfying_DES2_3":::  means :: AFF_3:def 8 (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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" "AP"  "st" (Bool (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 "P"))  ($#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"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "P"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "A"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "C"))))); end; 




:: deftheorem    defines :::"satisfying_DES2_3"::: AFF_3:def 8 :  (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v8_aff_3 :::"satisfying_DES2_3"::: )  ) "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 "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "," (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AP"))  "st" (Bool (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 "P"))  ($#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"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "P"))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Bool  "not"   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "c9")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c9"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "a9")) "," (Set (Var "p"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "q"))) & (Bool   ($#r1_aff_1 :::"LIN"::: )  (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "q"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a9")) "," (Set (Var "c9"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "q")))) "holds"  (Bool (Set (Var "A"))  ($#r5_aff_1 :::"//"::: )  (Set (Var "C")))))  ")" )); 
 
theorem :: AFF_3:1 (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "AP")) "is"   ($#v1_aff_3 :::"satisfying_DES1"::: )  )) "holds"  (Bool (Set (Var "AP")) "is"   ($#v2_aff_3 :::"satisfying_DES1_1"::: )  )) ; 
 
theorem :: AFF_3:2 (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "AP")) "is"   ($#v2_aff_3 :::"satisfying_DES1_1"::: )  )) "holds"  (Bool (Set (Var "AP")) "is"   ($#v1_aff_3 :::"satisfying_DES1"::: )  )) ; 
 
theorem :: AFF_3:3 (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"   ($#v1_aff_3 :::"satisfying_DES1"::: )  )) ; 
 
theorem :: AFF_3:4 (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"   ($#v3_aff_3 :::"satisfying_DES1_2"::: )  )) ; 
 
theorem :: AFF_3:5 (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "AP")) "is"   ($#v3_aff_3 :::"satisfying_DES1_2"::: )  )) "holds"  (Bool (Set (Var "AP")) "is"   ($#v4_aff_3 :::"satisfying_DES1_3"::: )  )) ; 
 
theorem :: AFF_3:6 (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "AP")) "is"   ($#v3_aff_3 :::"satisfying_DES1_2"::: )  )) "holds"  (Bool (Set (Var "AP")) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )) ; 
 
theorem :: AFF_3:7 (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "AP")) "is"   ($#v6_aff_3 :::"satisfying_DES2_1"::: )  )) "holds"  (Bool (Set (Var "AP")) "is"   ($#v5_aff_3 :::"satisfying_DES2"::: )  )) ; 
 
theorem :: AFF_3:8 (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v6_aff_3 :::"satisfying_DES2_1"::: )  ) "iff" (Bool (Set (Var "AP")) "is"   ($#v8_aff_3 :::"satisfying_DES2_3"::: )  )  ")" )) ; 
 
theorem :: AFF_3:9 (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::) "holds"   (Bool  "("  (Bool (Set (Var "AP")) "is"   ($#v5_aff_3 :::"satisfying_DES2"::: )  ) "iff" (Bool (Set (Var "AP")) "is"   ($#v7_aff_3 :::"satisfying_DES2_2"::: )  )  ")" )) ; 
 
theorem :: AFF_3:10 (Bool  "for" (Set (Var "AP")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "AP")) "is"   ($#v4_aff_3 :::"satisfying_DES1_3"::: )  )) "holds"  (Bool (Set (Var "AP")) "is"   ($#v6_aff_3 :::"satisfying_DES2_1"::: )  )) ;