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

A1: Cong m is_symmetric_in INT

hence Cong m is Equivalence_Relation of INT by A1, A5, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum

A1: Cong m is_symmetric_in INT

proof

A5:
Cong m is_transitive_in INT
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;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

proof

field (Cong m) = INT
by ORDERS_1:12;
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;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

hence Cong m is Equivalence_Relation of INT by A1, A5, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum