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 ;
then A5: (y \ u) \ (y \ v) in I by ;
((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 ;
then (y \ v) \ (y \ u) in I by ;
then A7: [(y \ u),(y \ v)] in RI by ;
((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 ;
then A10: (y \ u) \ (x \ u) in I by ;
x \ y in I by ;
then (x \ u) \ (y \ u) in I by ;
then [(x \ u),(y \ u)] in RI by ;
hence [(x \ u),(y \ v)] in RI by ; :: thesis: verum
end;
hence RI is Congruence of X by Def9; :: thesis: verum