let OAS be OAffinSpace; :: thesis: OAS is satisfying_Ext_Par_Pasch
let a be Element of OAS; :: according to PASCH:def 2 :: thesis: for b, c, d, p being Element of OAS st Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b holds
Mid p,a,d
let b, c, d, p be Element of OAS; :: thesis: ( Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b implies Mid p,a,d )
assume ( Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b ) ; :: thesis: Mid p,a,d
hence Mid p,a,d by Th15; :: thesis: verum