let X be BCI-algebra; for R being Equivalence_Relation of X holds
( R is Congruence of X iff ( R is R-congruence of X & R is L-congruence of X ) )
let R be Equivalence_Relation of X; ( R is Congruence of X iff ( R is R-congruence of X & R is L-congruence of X ) )
A1:
field R = the carrier of X
by EQREL_1:9;
then A2:
R is_reflexive_in the carrier of X
by RELAT_2:def 9;
thus
( R is Congruence of X implies ( R is R-congruence of X & R is L-congruence of X ) )
( R is R-congruence of X & R is L-congruence of X implies R is Congruence of X )proof
assume A3:
R is
Congruence of
X
;
( R is R-congruence of X & R is L-congruence of X )
thus
R is
R-congruence of
X
R is L-congruence of Xproof
let x,
y be
Element of
X;
BCIALG_2:def 11 ( [x,y] in R implies for u being Element of X holds [(x \ u),(y \ u)] in R )
assume A4:
[x,y] in R
;
for u being Element of X holds [(x \ u),(y \ u)] in R
let u be
Element of
X;
[(x \ u),(y \ u)] in R
[u,u] in R
by A2, RELAT_2:def 1;
hence
[(x \ u),(y \ u)] in R
by A3, A4, Def9;
verum
end;
let x,
y be
Element of
X;
BCIALG_2:def 10 ( [x,y] in R implies for u being Element of X holds [(u \ x),(u \ y)] in R )
assume A5:
[x,y] in R
;
for u being Element of X holds [(u \ x),(u \ y)] in R
let u be
Element of
X;
[(u \ x),(u \ y)] in R
[u,u] in R
by A2, RELAT_2:def 1;
hence
[(u \ x),(u \ y)] in R
by A3, A5, Def9;
verum
end;
assume A6:
( R is R-congruence of X & R is L-congruence of X )
; R is Congruence of X
A7:
R is_transitive_in the carrier of X
by A1, RELAT_2:def 16;
now for x, y, u, v being Element of X st [x,y] in R & [u,v] in R holds
[(x \ u),(y \ v)] in Rlet x,
y,
u,
v be
Element of
X;
( [x,y] in R & [u,v] in R implies [(x \ u),(y \ v)] in R )assume
(
[x,y] in R &
[u,v] in R )
;
[(x \ u),(y \ v)] in Rthen
(
[(x \ u),(y \ u)] in R &
[(y \ u),(y \ v)] in R )
by A6, Def10, Def11;
hence
[(x \ u),(y \ v)] in R
by A7, RELAT_2:def 8;
verum end;
hence
R is Congruence of X
by Def9; verum