theorem :: BCIIDEAL:57

for X being BCK-algebra
for I being Ideal of X st I is implicative-ideal of X holds
( I is commutative Ideal of X & I is positive-implicative-ideal of X )