for RI being I-congruence of X,A holds RI is Equivalence_Relation of X

proof

let RI be I-congruence of X,A; :: thesis: RI is Equivalence_Relation of X
reconsider RI = RI as Relation of X ;
RI is_reflexive_in the carrier of X

proof

for x being set st x in the carrier of X holds
[x,x] in RI

proof

let x be set ; :: thesis: ( x in the carrier of X implies [x,x] in RI )
assume x in the carrier of X ; :: thesis: [x,x] in RI
then reconsider x = x as Element of X ;
0. X in A by BCIALG_1:def 18;
then x \ x in A by BCIALG_1:def 5;
hence [x,x] in RI by Def12; :: thesis: verum

end;

hence RI is_reflexive_in the carrier of X by RELAT_2:def 1; :: thesis: verum

end;

then A2: field RI = the carrier of X by ORDERS_1:98;
A4: RI is symmetric

proof

for x, y being set st x in the carrier of X & y in the carrier of X & [x,y] in RI holds
[y,x] in RI

proof

let x, y be set ; :: thesis: ( x in the carrier of X & y in the carrier of X & [x,y] in RI implies [y,x] in RI )
assume A5: ( x in the carrier of X & y in the carrier of X & [x,y] in RI ) ; :: thesis: [y,x] in RI
then reconsider x = x, y = y as Element of X ;
( x \ y in A & y \ x in A ) by A5, Def12;
hence [y,x] in RI by Def12; :: thesis: verum

end;

then RI is_symmetric_in the carrier of X by RELAT_2:def 3;
hence RI is symmetric by A2, RELAT_2:def 11; :: thesis: verum

end;

RI is transitive

proof

for x, y, z being set st [x,y] in RI & [y,z] in RI holds
[x,z] in RI

proof

let x, y, z be set ; :: thesis: ( [x,y] in RI & [y,z] in RI implies [x,z] in RI )
assume A6: ( [x,y] in RI & [y,z] in RI ) ; :: thesis: [x,z] in RI
then reconsider x = x, y = y, z = z as Element of X by ZFMISC_1:106;
A7: ( x \ y in A & y \ x in A & y \ z in A & z \ y in A ) by A6, Def12;
((x \ z) \ (x \ y)) \ (y \ z) = 0. X by BCIALG_1:1;
then ((x \ z) \ (x \ y)) \ (y \ z) in A by BCIALG_1:def 18;
then (x \ z) \ (x \ y) in A by A7, BCIALG_1:def 18;
then A8: x \ z in A by A7, BCIALG_1:def 18;
((z \ x) \ (y \ x)) \ (z \ y) = 0. X by BCIALG_1:def 3;
then ((z \ x) \ (y \ x)) \ (z \ y) in A by BCIALG_1:def 18;
then (z \ x) \ (y \ x) in A by A7, BCIALG_1:def 18;
then z \ x in A by A7, BCIALG_1:def 18;
hence [x,z] in RI by A8, Def12; :: thesis: verum

end;

hence RI is transitive by RELAT_2:48; :: thesis: verum

end;

hence RI is Equivalence_Relation of X by A2, A4, EQREL_1:16; :: thesis: verum

end;

hence for b₁ being I-congruence of X,A holds
( b₁ is total & b₁ is symmetric & b₁ is transitive ) ; :: thesis: verum