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

A1: now :: thesis: for x, y being Element of X st x \ y in Class (E,(0. X)) & y in Class (E,(0. X)) holds
x in Class (E,(0. X))

let x, y be Element of X; :: thesis: ( x \ y in Class (E,(0. X)) & y in Class (E,(0. X)) implies x in Class (E,(0. X)) )
assume that
A2: x \ y in Class (E,(0. X)) and
A3: y in Class (E,(0. X)) ; :: thesis: x in Class (E,(0. X))
A4: [x,x] in E by EQREL_1:5;
[(0. X),y] in E by A3, EQREL_1:18;
then [(x \ (0. X)),(x \ y)] in E by A4, Def9;
then [x,(x \ y)] in E by BCIALG_1:2;
then A5: [(x \ y),x] in E by EQREL_1:6;
[(0. X),(x \ y)] in E by A2, EQREL_1:18;
then [(0. X),x] in E by A5, EQREL_1:7;
hence x in Class (E,(0. X)) by EQREL_1:18; :: thesis: verum

end;

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

now :: thesis: for x being Element of Rx holds x ` in Class (E,(0. X))

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

end;

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