:: deftheorem defines positive BCIIDEAL:def 2 :
for X being BCI-algebra
for I being Ideal of X holds
( I is positive iff for x being Element of I holds x is positive );