let m be Integer; Cong m is Equivalence_Relation of INT
A1:
Cong m is_symmetric_in INT
A5:
Cong m is_transitive_in INT
proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( 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 )
;
[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;
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; verum