:: deftheorem defines are_congruent_mod INT_1:def 5 :
for i1, i2, i3 being Integer holds
( i1,i2 are_congruent_mod i3 iff ex i4 being Integer st i3 * i4 = i1 - i2 );