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 ) )
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 ) ) :: thesis: ( 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 ; :: 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 X

proof

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 A4: [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 A2, RELAT_2:def 1;
hence [(x \ u),(y \ u)] in R by A3, A4, 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 A5: [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 A2, RELAT_2:def 1;
hence [(u \ x),(u \ y)] in R by A3, A5, Def9; :: thesis: verum

end;

assume A6: ( R is R-congruence of X & R is L-congruence of X ) ; :: thesis: R is Congruence of X
A7: R is_transitive_in the carrier of X by A1, RELAT_2:def 16;

now :: thesis: for x, y, u, v being Element of X st [x,y] in R & [u,v] in R holds
[(x \ u),(y \ v)] in R

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 R
then ( [(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; :: thesis: verum

end;

hence R is Congruence of X by Def9; :: thesis: verum