let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( between a,b,c & between b,a,c implies a = b )

assume H1: between a,b,c ; :: thesis: ( not between b,a,c or a = b )

assume between b,a,c ; :: thesis: 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; :: thesis: verum

a = b

let a, b, c be POINT of S; :: thesis: ( between a,b,c & between b,a,c implies a = b )

assume H1: between a,b,c ; :: thesis: ( not between b,a,c or a = b )

assume between b,a,c ; :: thesis: 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; :: thesis: verum