:: deftheorem Def1 defines Cong INT_4:def 1 :
for m being Integer
for b₂ being Relation of INT holds
( b₂ = Cong m iff for x, y being Integer holds
( [x,y] in b₂ iff x,y are_congruent_mod m ) );