let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, p, q, z being POINT of S st between a,p,z & between b,q,z holds

ex x being POINT of S st

( between p,x,b & between q,x,a )

let a, b, p, q, z be POINT of S; :: thesis: ( between a,p,z & between b,q,z implies ex x being POINT of S st

( between p,x,b & between q,x,a ) )

S is satisfying_Pasch ;

hence ( between a,p,z & between b,q,z implies ex x being POINT of S st

( between p,x,b & between q,x,a ) ) ; :: thesis: verum

ex x being POINT of S st

( between p,x,b & between q,x,a )

let a, b, p, q, z be POINT of S; :: thesis: ( between a,p,z & between b,q,z implies ex x being POINT of S st

( between p,x,b & between q,x,a ) )

S is satisfying_Pasch ;

hence ( between a,p,z & between b,q,z implies ex x being POINT of S st

( between p,x,b & between q,x,a ) ) ; :: thesis: verum