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