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