let X be BCI-algebra; :: thesis: for I being Ideal of X st ( for x being Element of X holds x \ ((0. X) \ x) in I ) holds
I is closed Ideal of X
let I be Ideal of X; :: thesis: ( ( for x being Element of X holds x \ ((0. X) \ x) in I ) implies I is closed Ideal of X )
assume A1: for x being Element of X holds x \ ((0. X) \ x) in I ; :: thesis: I is closed Ideal of X
for x1 being Element of I holds x1 ` in I

proof

let x1 be Element of I; :: thesis: x1 ` in I
((0. X) \ x1) \ x1 = ((0. X) \ ((0. X) \ ((0. X) \ x1))) \ x1 by BCIALG_1:8;
then ((0. X) \ x1) \ x1 = ((0. X) \ x1) \ ((0. X) \ ((0. X) \ x1)) by BCIALG_1:7;
then ((0. X) \ x1) \ x1 in I by A1;
hence x1 ` in I by BCIALG_1:def 18; :: thesis: verum

end;

hence I is closed Ideal of X by BCIALG_1:def 19; :: thesis: verum