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

between z,p,a

let a, p, z be POINT of S; :: thesis: ( between a,p,z implies between z,p,a )

assume H1: between a,p,z ; :: thesis: between z,p,a

between p,z,z by Bqaa;

then consider x being POINT of S such that

X1: ( between p,x,p & between z,x,a ) by H1, A7;

thus between z,p,a by X1, A6; :: thesis: verum

between z,p,a

let a, p, z be POINT of S; :: thesis: ( between a,p,z implies between z,p,a )

assume H1: between a,p,z ; :: thesis: between z,p,a

between p,z,z by Bqaa;

then consider x being POINT of S such that

X1: ( between p,x,p & between z,x,a ) by H1, A7;

thus between z,p,a by X1, A6; :: thesis: verum