let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: verum