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