let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( between a,p,z implies between z,p,a )
assume H1:
between a,p,z
; 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; verum