let OAS be OAffinSpace; :: thesis: OAS is satisfying_Gen_Par_Pasch
let a be Element of OAS; :: according to PASCH:def 3 :: thesis: for b, c, a9, b9, c9 being Element of OAS st not LIN a,b,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 holds
Mid a9,b9,c9
let b, c, a9, b9, c9 be Element of OAS; :: thesis: ( not LIN a,b,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 implies Mid a9,b9,c9 )
assume that
A1: not LIN a,b,a9 and
A2: a,a9 '||' b,b9 and
A3: a,a9 '||' c,c9 and
A4: Mid a,b,c and
A5: LIN a9,b9,c9 ; :: thesis: Mid a9,b9,c9
thus Mid a9,b9,c9 by A1, A2, A3, A4, A5, Th17; :: thesis: verum