:: PASCH  semantic presentation begin  


























definitionlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); attr "OAS" is  :::"satisfying_Int_Par_Pasch":::  means :: PASCH:def 1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS"  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "a"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "d")) "," (Set (Var "a")))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "d")))); end; 




:: deftheorem    defines :::"satisfying_Int_Par_Pasch"::: PASCH:def 1 :  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "OAS")) "is"   ($#v1_pasch :::"satisfying_Int_Par_Pasch"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "a"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "d")) "," (Set (Var "a")))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "d"))))  ")" )); 
 definitionlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); attr "OAS" is  :::"satisfying_Ext_Par_Pasch":::  means :: PASCH:def 2 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS"  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b"))))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "d")))); end; 




:: deftheorem    defines :::"satisfying_Ext_Par_Pasch"::: PASCH:def 2 :  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "OAS")) "is"   ($#v2_pasch :::"satisfying_Ext_Par_Pasch"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b"))))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "d"))))  ")" )); 
 definitionlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); attr "OAS" is  :::"satisfying_Gen_Par_Pasch":::  means :: PASCH:def 3 (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" "OAS"  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "c9"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")))); end; 




:: deftheorem    defines :::"satisfying_Gen_Par_Pasch"::: PASCH:def 3 :  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "OAS")) "is"   ($#v3_pasch :::"satisfying_Gen_Par_Pasch"::: )  ) "iff" (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 "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "c9"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9"))))  ")" )); 
 definitionlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); attr "OAS" is  :::"satisfying_Ext_Bet_Pasch":::  means :: PASCH:def 4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS"  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "c"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS" "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "y")) "," (Set (Var "c"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "d")))  ")" ))); end; 




:: deftheorem    defines :::"satisfying_Ext_Bet_Pasch"::: PASCH:def 4 :  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "OAS")) "is"   ($#v4_pasch :::"satisfying_Ext_Bet_Pasch"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "c"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "y")) "," (Set (Var "c"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "d")))  ")" )))  ")" )); 
 definitionlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); attr "OAS" is  :::"satisfying_Int_Bet_Pasch":::  means :: PASCH:def 5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS"  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "c"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS" "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "y")) "," (Set (Var "c"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "d")))  ")" ))); end; 




:: deftheorem    defines :::"satisfying_Int_Bet_Pasch"::: PASCH:def 5 :  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "OAS")) "is"   ($#v5_pasch :::"satisfying_Int_Bet_Pasch"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "c"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "y")) "," (Set (Var "c"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "d")))  ")" )))  ")" )); 
 definitionlet "OAS" be   ($#l1_analoaf :::"OAffinSpace":::); attr "OAS" is  :::"Fanoian":::  means :: PASCH:def 6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS"  "st" (Bool (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"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "OAS" "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "d"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "c")))  ")" ))); end; 




:: deftheorem    defines :::"Fanoian"::: PASCH:def 6 :  (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "OAS")) "is"   ($#v6_pasch :::"Fanoian"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (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"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "d"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "c")))  ")" )))  ")" )); 
 
theorem :: PASCH:1 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "b")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "c"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p")))) "holds"  (Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d")))  ")" )))) ; 
 
theorem :: PASCH:2 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "c"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p")))) "holds"  (Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d")))  ")" )))) ; 
 
theorem :: PASCH:3 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "c"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "p")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d")))  ")" )))) ; 
 
theorem :: PASCH:4 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "d1"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "d2"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d2")))) "holds"  (Bool (Set (Var "d1"))  ($#r1_hidden :::"="::: )  (Set (Var "d2"))))) ; 
 
theorem :: PASCH:5 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d2"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d1"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d2")))) "holds"  (Bool (Set (Var "d1"))  ($#r1_hidden :::"="::: )  (Set (Var "d2"))))) ; 
 
theorem :: PASCH:6 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "p")) "," (Set (Var "a"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "d")) "," (Set (Var "a")))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "c")) "," (Set (Var "p")) "," (Set (Var "d"))))) ; 
 
theorem :: PASCH:7 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"  (Bool (Set (Var "OAS")) "is"   ($#v1_pasch :::"satisfying_Int_Par_Pasch"::: )  )) ; 
 
theorem :: PASCH:8 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b"))))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "d"))))) ; 
 
theorem :: PASCH:9 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"  (Bool (Set (Var "OAS")) "is"   ($#v2_pasch :::"satisfying_Ext_Par_Pasch"::: )  )) ; 
 
theorem :: PASCH:10 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "c9"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9"))))) ; 
 
theorem :: PASCH:11 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"  (Bool (Set (Var "OAS")) "is"   ($#v3_pasch :::"satisfying_Gen_Par_Pasch"::: )  )) ; 
 
theorem :: PASCH:12 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "a9"))) & (Bool (Set (Var "b")) "," (Set (Var "p"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "a9")) "," (Set (Var "b9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b9")) "," (Set (Var "a9"))))) ; 
 
theorem :: PASCH:13 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "b")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "a9")))) & (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b"))) & (Bool (Set (Var "p")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b9"))) & (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "b9")))) "holds"  (Bool (Set (Var "a")) "," (Set (Var "a9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b9"))))) ; 
 
theorem :: PASCH:14 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "p")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "a")) "," (Set (Var "c")))) "holds"  (Bool  "("  (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "p")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "c")))  ")" ))) ; 
 
theorem :: PASCH:15 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "b"))) & (Bool (Set (Var "c")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "p")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "a"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "d")) "," (Set (Var "a"))))) ; 
 
theorem :: PASCH:16 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "d")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "d")) "," (Set (Var "a"))) & (Bool (Set (Var "c")) "," (Set (Var "d"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "a"))) & (Bool (Set (Var "p")) "," (Set (Var "c"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "b"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c")))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "b"))))) ; 
 
theorem :: PASCH:17 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool (Set (Var "p")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "c"))) & (Bool (Set (Var "b")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d")))) "holds"  (Bool  "not" (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "d")))))) ; 
 
theorem :: PASCH:18 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p")) "," (Set (Var "x"))) & (Bool (Set (Var "b")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "x")))  ")" )))) ; 
 
theorem :: PASCH:19 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "a"))) & (Bool (Set (Var "b")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "x")))  ")" )))) ; 
 
theorem :: PASCH:20 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "x"))) & (Bool (Set (Var "b")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "x")))  ")" )))) ; 
 
theorem :: PASCH:21 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "a"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "x")) "," (Set (Var "c")))  ")" )))) ; 
 
theorem :: PASCH:22 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "x"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "c"))) & (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "x")) "," (Set (Var "c")))  ")" )))) ; 
 
theorem :: PASCH:23 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_analoaf :::"//"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "d"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "c")))  ")" )))) ; 
 
theorem :: PASCH:24 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"  (Bool (Set (Var "OAS")) "is"   ($#v6_pasch :::"Fanoian"::: )  )) ; 
 
theorem :: PASCH:25 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Set (Var "a")) "," (Set (Var "c"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "b")) "," (Set (Var "d"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "d"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "c")))  ")" )))) ; 
 
theorem :: PASCH:26 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "p")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_diraf :::"'||'"::: )  (Set (Var "c")) "," (Set (Var "d"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "d"))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "c")))) "holds"  (Bool  "not" (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")))))) ; 
 
theorem :: PASCH:27 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "x")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "c"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "y")) "," (Set (Var "c"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "d")))  ")" )))) ; 
 
theorem :: PASCH:28 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"  (Bool (Set (Var "OAS")) "is"   ($#v4_pasch :::"satisfying_Ext_Bet_Pasch"::: )  )) ; 
 
theorem :: PASCH:29 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "x")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "c"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))))) "holds"  (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS")) "st"  (Bool  "("  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "b")) "," (Set (Var "y")) "," (Set (Var "c"))) & (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "d")))  ")" )))) ; 
 
theorem :: PASCH:30 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::) "holds"  (Bool (Set (Var "OAS")) "is"   ($#v5_pasch :::"satisfying_Int_Bet_Pasch"::: )  )) ; 
 
theorem :: PASCH:31 (Bool  "for" (Set (Var "OAS")) "being"   ($#l1_analoaf :::"OAffinSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "p9")) "," (Set (Var "a9")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "OAS"))  "st" (Bool (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "p")) "," (Set (Var "a"))  ($#r2_analoaf :::"//"::: )  (Set (Var "p9")) "," (Set (Var "a9"))) & (Bool (Bool  "not"   ($#r3_diraf :::"LIN"::: )  (Set (Var "p")) "," (Set (Var "a")) "," (Set (Var "p9")))) & (Bool   ($#r3_diraf :::"LIN"::: )  (Set (Var "p9")) "," (Set (Var "a9")) "," (Set (Var "b9"))) & (Bool (Set (Var "p")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "a")) "," (Set (Var "a9"))) & (Bool (Set (Var "p")) "," (Set (Var "p9"))  ($#r2_analoaf :::"//"::: )  (Set (Var "b")) "," (Set (Var "b9")))) "holds"  (Bool   ($#r1_diraf :::"Mid"::: )  (Set (Var "p9")) "," (Set (Var "a9")) "," (Set (Var "b9"))))) ;