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
field RI = the carrier of X by EQREL_1:9;
then A1: RI is_transitive_in the carrier of X by RELAT_2:def 16;

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

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 that
A2: [x,y] in RI and
A3: [u,v] in RI ; :: thesis: [(x \ u),(y \ v)] in RI
((y \ u) \ (y \ v)) \ (v \ u) = 0. X by BCIALG_1:1;
then A4: ((y \ u) \ (y \ v)) \ (v \ u) in I by BCIALG_1:def 18;
v \ u in I by A3, Def12;
then A5: (y \ u) \ (y \ v) in I by A4, BCIALG_1:def 18;
((y \ v) \ (y \ u)) \ (u \ v) = 0. X by BCIALG_1:1;
then A6: ((y \ v) \ (y \ u)) \ (u \ v) in I by BCIALG_1:def 18;
u \ v in I by A3, Def12;
then (y \ v) \ (y \ u) in I by A6, BCIALG_1:def 18;
then A7: [(y \ u),(y \ v)] in RI by A5, Def12;
((x \ u) \ (y \ u)) \ (x \ y) = 0. X by BCIALG_1:def 3;
then A8: ((x \ u) \ (y \ u)) \ (x \ y) in I by BCIALG_1:def 18;
((y \ u) \ (x \ u)) \ (y \ x) = 0. X by BCIALG_1:def 3;
then A9: ((y \ u) \ (x \ u)) \ (y \ x) in I by BCIALG_1:def 18;
y \ x in I by A2, Def12;
then A10: (y \ u) \ (x \ u) in I by A9, BCIALG_1:def 18;
x \ y in I by A2, Def12;
then (x \ u) \ (y \ u) in I by A8, BCIALG_1:def 18;
then [(x \ u),(y \ u)] in RI by A10, Def12;
hence [(x \ u),(y \ v)] in RI by A1, A7, RELAT_2:def 8; :: thesis: verum

end;

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