theorem :: BCIIDEAL:17

for X being BCI-algebra
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