:: deftheorem Def7 defines implicative-ideal BCIIDEAL:def 7 :
for X being BCK-algebra
for b₂ being non empty Subset of X holds
( b₂ is implicative-ideal of X iff ( 0. X in b₂ & ( for x, y, z being Element of X st (x \ (y \ x)) \ z in b₂ & z in b₂ holds
x in b₂ ) ) );