let OAS be OAffinSpace; :: thesis: OAS is satisfying_Ext_Bet_Pasch
let a be Element of OAS; :: according to PASCH:def 4 :: thesis: for b, c, d, x, y being Element of OAS st Mid a,b,d & Mid b,x,c & not LIN a,b,c holds
ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )
let b, c, d, x, y be Element of OAS; :: thesis: ( Mid a,b,d & Mid b,x,c & not LIN a,b,c implies ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) )
assume that
A1: Mid a,b,d and
A2: Mid b,x,c and
A3: not LIN a,b,c ; :: thesis: ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )
thus ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) by A1, A2, A3, Th35; :: thesis: verum