let X be associative BCI-algebra; :: thesis: for A being Ideal of X holds A is closed
let A be Ideal of X; :: thesis: A is closed
for x being Element of A holds x ` in A

proof

let x be Element of A; :: thesis: x ` in A
(0. X) \ x = x \ (0. X) by BCIALG_1:48
.= x by BCIALG_1:2 ;
hence x ` in A ; :: thesis: verum

end;

hence A is closed ; :: thesis: verum