let X be BCI-algebra; :: thesis: for LC being L-congruence of X holds Class LC,(0. X) is closed Ideal of X
let LC be L-congruence of X; :: thesis: Class LC,(0. X) is closed Ideal of X

A1: now

let x, y be Element of X; :: thesis: ( x \ y in Class LC,(0. X) & y in Class LC,(0. X) implies x in Class LC,(0. X) )
assume that
A2: x \ y in Class LC,(0. X) and
A3: y in Class LC,(0. X) ; :: thesis: x in Class LC,(0. X)
[(0. X),y] in LC by A3, EQREL_1:26;
then [(x \ (0. X)),(x \ y)] in LC by Def10;
then [x,(x \ y)] in LC by BCIALG_1:2;
then A4: [(x \ y),x] in LC by EQREL_1:12;
[(0. X),(x \ y)] in LC by A2, EQREL_1:26;
then [(0. X),x] in LC by A4, EQREL_1:13;
hence x in Class LC,(0. X) by EQREL_1:26; :: thesis: verum

end;

[(0. X),(0. X)] in LC by EQREL_1:11;
then 0. X in Class LC,(0. X) by EQREL_1:26;
then reconsider Rx = Class LC,(0. X) as Ideal of X by A1, BCIALG_1:def 18;

now

let x be Element of Rx; :: thesis: x ` in Class LC,(0. X)
[(0. X),x] in LC by EQREL_1:26;
then [((0. X) ` ),(x ` )] in LC by Def10;
then [(0. X),(x ` )] in LC by BCIALG_1:def 5;
hence x ` in Class LC,(0. X) by EQREL_1:26; :: thesis: verum

end;

hence Class LC,(0. X) is closed Ideal of X by BCIALG_1:def 19; :: thesis: verum