let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b being POINT of S holds

( between a,a,a & a,a equiv b,b )

let a, b be POINT of S; :: thesis: ( between a,a,a & a,a equiv b,b )

consider x being POINT of S such that

Z1: ( between a,a,x & a,x equiv b,b ) by A4;

thus ( between a,a,a & a,a equiv b,b ) by Z1, A3; :: thesis: verum

( between a,a,a & a,a equiv b,b )

let a, b be POINT of S; :: thesis: ( between a,a,a & a,a equiv b,b )

consider x being POINT of S such that

Z1: ( between a,a,x & a,x equiv b,b ) by A4;

thus ( between a,a,a & a,a equiv b,b ) by Z1, A3; :: thesis: verum