:: PARDEPAP  semantic presentation begin  



theorem :: PARDEPAP:1 (Bool  "for" (Set (Var "SAS")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "SAS")) "is"   ($#v2_aff_2 :::"Pappian"::: )  )) "holds"  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS"))  "st" (Bool (Bool (Set (Var "a1")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a1")) "," (Set (Var "a3"))) & (Bool (Set (Var "b1")) "," (Set (Var "b2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b3"))) & (Bool (Set (Var "a1")) "," (Set (Var "b2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a2")) "," (Set (Var "b3"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a3")) "," (Set (Var "b2")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "b1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a1")) "," (Set (Var "b3"))))) ; 
 
theorem :: PARDEPAP:2 (Bool  "for" (Set (Var "SAS")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "SAS")) "is"   ($#v4_aff_2 :::"Desarguesian"::: )  )) "holds"  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b")))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "c")))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a9"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b9"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "c9"))) & (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"))))) ; 
 
theorem :: PARDEPAP:3 (Bool  "for" (Set (Var "SAS")) "being"   ($#l1_analoaf :::"AffinPlane":::)  "st" (Bool (Bool (Set (Var "SAS")) "is"   ($#v11_aff_2 :::"translational"::: )  )) "holds"  (Bool  "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "c9"))) & (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"))))) ; 
 
theorem :: PARDEPAP:4 (Bool  "ex" (Set (Var "SAS")) "being"   ($#l1_analoaf :::"AffinPlane":::) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "o")) "," (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b")))) & (Bool (Bool  "not" (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "c")))) & (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "a9"))) & (Bool (Set (Var "o")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b9"))) & (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "c9"))) & (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")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "c9"))) & (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")))  ")" ) & (Bool  "("   "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS"))  "st" (Bool (Bool (Set (Var "a1")) "," (Set (Var "a2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a1")) "," (Set (Var "a3"))) & (Bool (Set (Var "b1")) "," (Set (Var "b2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b1")) "," (Set (Var "b3"))) & (Bool (Set (Var "a1")) "," (Set (Var "b2"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a2")) "," (Set (Var "b1"))) & (Bool (Set (Var "a2")) "," (Set (Var "b3"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a3")) "," (Set (Var "b2")))) "holds"  (Bool (Set (Var "a3")) "," (Set (Var "b1"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a1")) "," (Set (Var "b3")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS"))  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "d")))) "holds"  (Bool  "not" (Bool (Set (Var "a")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))))  ")" )  ")" )) ; 
 
theorem :: PARDEPAP:5 (Bool  "for" (Set (Var "SAS")) "being"   ($#l1_analoaf :::"AffinPlane":::)  (Bool  "for" (Set (Var "o")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st"  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "holds"   (Bool  "("  (Bool (Set (Var "o")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "p"))) & (Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SAS")) "st"  (Bool  "("  (Bool (Bool (Set (Var "o")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "b")))) "implies" (Bool  "("  (Bool (Set (Var "o")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "o")) "," (Set (Var "d"))) & (Bool (Set (Var "p")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "d")))  ")" )  ")" ))  ")" ))))) ;