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