for RI being I-congruence of X,A holds RI is Equivalence_Relation of X
proof
let RI be
I-congruence of
X,
A;
RI is Equivalence_Relation of X
reconsider RI =
RI as
Relation of
X ;
for
x being
object st
x in the
carrier of
X holds
[x,x] in RI
then
RI is_reflexive_in the
carrier of
X
by RELAT_2:def 1;
then A1:
field RI = the
carrier of
X
by ORDERS_1:13;
for
x,
y,
z being
object st
[x,y] in RI &
[y,z] in RI holds
[x,z] in RI
proof
let x,
y,
z be
object ;
( [x,y] in RI & [y,z] in RI implies [x,z] in RI )
assume that A2:
[x,y] in RI
and A3:
[y,z] in RI
;
[x,z] in RI
reconsider x =
x,
y =
y,
z =
z as
Element of
X by A2, A3, ZFMISC_1:87;
((z \ x) \ (y \ x)) \ (z \ y) = 0. X
by BCIALG_1:def 3;
then A4:
((z \ x) \ (y \ x)) \ (z \ y) in A
by BCIALG_1:def 18;
((x \ z) \ (x \ y)) \ (y \ z) = 0. X
by BCIALG_1:1;
then A5:
((x \ z) \ (x \ y)) \ (y \ z) in A
by BCIALG_1:def 18;
y \ z in A
by A3, Def12;
then A6:
(x \ z) \ (x \ y) in A
by A5, BCIALG_1:def 18;
z \ y in A
by A3, Def12;
then A7:
(z \ x) \ (y \ x) in A
by A4, BCIALG_1:def 18;
y \ x in A
by A2, Def12;
then A8:
z \ x in A
by A7, BCIALG_1:def 18;
x \ y in A
by A2, Def12;
then
x \ z in A
by A6, BCIALG_1:def 18;
hence
[x,z] in RI
by A8, Def12;
verum
end;
then A9:
RI is
transitive
by RELAT_2:31;
for
x,
y being
object st
x in the
carrier of
X &
y in the
carrier of
X &
[x,y] in RI holds
[y,x] in RI
then
RI is_symmetric_in the
carrier of
X
by RELAT_2:def 3;
then
RI is
symmetric
by A1, RELAT_2:def 11;
hence
RI is
Equivalence_Relation of
X
by A1, A9, EQREL_1:9;
verum
end;
hence
for b1 being I-congruence of X,A holds
( b1 is total & b1 is symmetric & b1 is transitive )
; verum