let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds
p,q equiv r,s
let a, b, p, q, r, s be POINT of S; ( a,b equiv p,q & a,b equiv r,s implies p,q equiv r,s )
S is satisfying_CongruenceEquivalenceRelation
;
hence
( a,b equiv p,q & a,b equiv r,s implies p,q equiv r,s )
; verum