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