let m be Integer; :: thesis: Cong m is Equivalence_Relation of INT
A1: Cong m is_symmetric_in INT
proof
let x, y be object ; :: 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 that
A2: x in INT and
A3: y in INT and
A4: [x,y] in Cong m ; :: thesis: [y,x] in Cong m
reconsider y = y as Integer by A3;
reconsider x = x as Integer by A2;
x,y are_congruent_mod m by A4, Def1;
then y,x are_congruent_mod m by INT_1:14;
hence [y,x] in Cong m by Def1; :: thesis: verum
end;
A5: Cong m is_transitive_in INT
proof
let x, y, z be object ; :: 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 that
A6: ( x in INT & y in INT & z in INT ) and
A7: ( [x,y] in Cong m & [y,z] in Cong m ) ; :: thesis: [x,z] in Cong m
reconsider x = x, y = y, z = z as Integer by A6;
( x,y are_congruent_mod m & y,z are_congruent_mod m ) by A7, Def1;
then x,z are_congruent_mod m by INT_1:15;
hence [x,z] in Cong m by Def1; :: thesis: verum
end;
field (Cong m) = INT by ORDERS_1:12;
hence Cong m is Equivalence_Relation of INT by A1, A5, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum