let X be BCI-algebra; :: thesis: 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; :: thesis: ( R is Congruence of X iff ( R is R-congruence of X & R is L-congruence of X ) )
( R is reflexive & R is symmetric & R is transitive & field R = the carrier of X )
by EQREL_1:16;
then A1:
( R is_reflexive_in the carrier of X & R is_symmetric_in the carrier of X & R is_transitive_in the carrier of X )
by RELAT_2:def 9, RELAT_2:def 11, RELAT_2:def 16;
thus
( R is Congruence of X implies ( R is R-congruence of X & R is L-congruence of X ) )
:: thesis: ( R is R-congruence of X & R is L-congruence of X implies R is Congruence of X )proof
assume A2:
R is
Congruence of
X
;
:: thesis: ( R is R-congruence of X & R is L-congruence of X )
thus
R is
R-congruence of
X
:: thesis: R is L-congruence of Xproof
let x,
y be
Element of
X;
:: according to BCIALG_2:def 11 :: thesis: ( [x,y] in R implies for u being Element of X holds [(x \ u),(y \ u)] in R )
assume A3:
[x,y] in R
;
:: thesis: for u being Element of X holds [(x \ u),(y \ u)] in R
let u be
Element of
X;
:: thesis: [(x \ u),(y \ u)] in R
[u,u] in R
by A1, RELAT_2:def 1;
hence
[(x \ u),(y \ u)] in R
by A2, A3, Def9;
:: thesis: verum
end;
let x,
y be
Element of
X;
:: according to BCIALG_2:def 10 :: thesis: ( [x,y] in R implies for u being Element of X holds [(u \ x),(u \ y)] in R )
assume A4:
[x,y] in R
;
:: thesis: for u being Element of X holds [(u \ x),(u \ y)] in R
let u be
Element of
X;
:: thesis: [(u \ x),(u \ y)] in R
[u,u] in R
by A1, RELAT_2:def 1;
hence
[(u \ x),(u \ y)] in R
by A2, A4, Def9;
:: thesis: verum
end;
assume A5:
( R is R-congruence of X & R is L-congruence of X )
; :: thesis: R is Congruence of X
now let x,
y,
u,
v be
Element of
X;
:: thesis: ( [x,y] in R & [u,v] in R implies [(x \ u),(y \ v)] in R )assume
(
[x,y] in R &
[u,v] in R )
;
:: thesis: [(x \ u),(y \ v)] in Rthen
(
[(x \ u),(y \ u)] in R &
[(y \ u),(y \ v)] in R )
by A5, Def10, Def11;
hence
[(x \ u),(y \ v)] in R
by A1, RELAT_2:def 8;
:: thesis: verum end;
hence
R is Congruence of X
by Def9; :: thesis: verum