let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c being POINT of S st between a,b,c & between b,a,c holds
a = b
let a, b, c be POINT of S; ( between a,b,c & between b,a,c implies a = b )
assume H1:
between a,b,c
; ( not between b,a,c or a = b )
assume
between b,a,c
; a = b
then consider x being POINT of S such that
X1:
( between b,x,b & between a,x,a )
by H1, A7;
b = x
by X1, A6;
hence
a = b
by A6, X1; verum