theorem :: BCIIDEAL:16

for X being BCI-algebra
for I being Ideal of X st I is associative-ideal of X holds
for x being Element of X holds x \ ((0. X) \ x) in I