:: deftheorem defines satisfying_CongruenceEquivalenceRelation GTARSKI1:def 6 :
for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceEquivalenceRelation iff 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 );