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: [(0. X),(0. X)] in E by EQREL_1:11;
Class E,(0. X) is Ideal of X

proof

A2: 0. X in Class E,(0. X) by A1, EQREL_1:26;

now

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 ( x \ y in Class E,(0. X) & y in Class E,(0. X) ) ; :: thesis: x in Class E,(0. X)
then A3: ( [(0. X),(x \ y)] in E & [(0. X),y] in E ) by EQREL_1:26;
[x,x] in E by EQREL_1:11;
then [(x \ (0. X)),(x \ y)] in E by A3, Def9;
then [x,(x \ y)] in E by BCIALG_1:2;
then [(x \ y),x] in E by EQREL_1:12;
then [(0. X),x] in E by A3, EQREL_1:13;
hence x in Class E,(0. X) by EQREL_1:26; :: thesis: verum

end;

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

end;

then reconsider Rx = Class E,(0. X) as Ideal of X ;
Rx is closed

proof

now

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

end;

hence Rx is closed by BCIALG_1:def 19; :: thesis: verum

end;

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