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

a = b

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

S is satisfying_BetweennessIdentity ;

hence ( between a,b,a implies a = b ) ; :: thesis: verum

a = b

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

S is satisfying_BetweennessIdentity ;

hence ( between a,b,a implies a = b ) ; :: thesis: verum