:: deftheorem Def2 defines CONGRD TDGROUP:def 2 :
for ADG being non empty addLoopStr
for b₂ being Relation of [: the carrier of ADG, the carrier of ADG:] holds
( b₂ = CONGRD ADG iff for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in b₂ iff a # d = b # c ) );