theorem :: BCIIDEAL:56

for X being BCK-algebra
for I, A being Ideal of X st I c= A & I is positive-implicative-ideal of X holds
A is positive-implicative-ideal of X