:: deftheorem Def18 defines Ideal BCIALG_1:def 18 :
for X being BCI-algebra
for b₂ being non empty Subset of X holds
( b₂ is Ideal of X iff ( 0. X in b₂ & ( for x, y being Element of X st x \ y in b₂ & y in b₂ holds
x in b₂ ) ) );