let m be Integer; :: thesis: Cong m is Equivalence_Relation of INT
A1: Cong m is_symmetric_in INT

proof

let x, y be set ; :: according to RELAT_2:def 3 :: thesis: ( not x in INT or not y in INT or not [x,y] in Cong m or [y,x] in Cong m )
assume A2: ( x in INT & y in INT & [x,y] in Cong m ) ; :: thesis: [y,x] in Cong m
then reconsider x = x as Integer ;
reconsider y = y as Integer by A2;
x,y are_congruent_mod m by A2, Def1;
then y,x are_congruent_mod m by INT_1:35;
hence [y,x] in Cong m by Def1; :: thesis: verum

end;

A3: Cong m is_transitive_in INT

proof

let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in INT or not y in INT or not z in INT or not [x,y] in Cong m or not [y,z] in Cong m or [x,z] in Cong m )
assume A4: ( x in INT & y in INT & z in INT & [x,y] in Cong m & [y,z] in Cong m ) ; :: thesis: [x,z] in Cong m
then reconsider x = x, y = y, z = z as Integer ;
( x,y are_congruent_mod m & y,z are_congruent_mod m ) by A4, Def1;
then x,z are_congruent_mod m by INT_1:36;
hence [x,z] in Cong m by Def1; :: thesis: verum

end;

field (Cong m) = INT by ORDERS_1:97;
hence Cong m is Equivalence_Relation of INT by A1, A3, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum