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

a = b

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

S is satisfying_CongruenceIdentity ;

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

a = b

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

S is satisfying_CongruenceIdentity ;

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