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