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