let X be BCI-algebra; :: thesis: for I being Ideal of X
for RI being I-congruence of X,I holds RI is Congruence of X
let I be Ideal of X; :: thesis: for RI being I-congruence of X,I holds RI is Congruence of X
let RI be I-congruence of X,I; :: thesis: RI is Congruence of X
( RI is reflexive & RI is symmetric & RI is transitive & field RI = the carrier of X ) by EQREL_1:16;
then A1: RI is_transitive_in the carrier of X by RELAT_2:def 16;

now

let x, y, u, v be Element of X; :: thesis: ( [x,y] in RI & [u,v] in RI implies [(x \ u),(y \ v)] in RI )
assume ( [x,y] in RI & [u,v] in RI ) ; :: thesis: [(x \ u),(y \ v)] in RI
then A2: ( x \ y in I & y \ x in I & u \ v in I & v \ u in I ) by Def12;
( ((x \ u) \ (y \ u)) \ (x \ y) = 0. X & ((y \ u) \ (x \ u)) \ (y \ x) = 0. X ) by BCIALG_1:def 3;
then ( ((x \ u) \ (y \ u)) \ (x \ y) in I & ((y \ u) \ (x \ u)) \ (y \ x) in I ) by BCIALG_1:def 18;
then ( (x \ u) \ (y \ u) in I & (y \ u) \ (x \ u) in I ) by A2, BCIALG_1:def 18;
then A3: [(x \ u),(y \ u)] in RI by Def12;
( ((y \ u) \ (y \ v)) \ (v \ u) = 0. X & ((y \ v) \ (y \ u)) \ (u \ v) = 0. X ) by BCIALG_1:1;
then ( ((y \ u) \ (y \ v)) \ (v \ u) in I & ((y \ v) \ (y \ u)) \ (u \ v) in I ) by BCIALG_1:def 18;
then ( (y \ u) \ (y \ v) in I & (y \ v) \ (y \ u) in I ) by A2, BCIALG_1:def 18;
then [(y \ u),(y \ v)] in RI by Def12;
hence [(x \ u),(y \ v)] in RI by A1, A3, RELAT_2:def 8; :: thesis: verum

end;

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