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 that
A1: Mid p,b,c and
A2: LIN p,a,d and
A3: a,b '||' c,d and
A4: not LIN p,a,b ; :: thesis: Mid p,a,d
thus Mid p,a,d by A1, A2, A3, A4, Th15; :: thesis: verum