let X be BCK-algebra; :: thesis: 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
let I, A be Ideal of X; :: thesis: ( I c= A & I is positive-implicative-ideal of X implies A is positive-implicative-ideal of X )
assume that
A1: I c= A and
A2: I is positive-implicative-ideal of X ; :: thesis: A is positive-implicative-ideal of X
for x, y being Element of X st (x \ y) \ y in A holds
x \ y in A

proof

let x, y be Element of X; :: thesis: ( (x \ y) \ y in A implies x \ y in A )
((x \ ((x \ y) \ y)) \ y) \ y = ((x \ y) \ ((x \ y) \ y)) \ y by BCIALG_1:7
.= ((x \ y) \ y) \ ((x \ y) \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
then ((x \ ((x \ y) \ y)) \ y) \ y in I by BCIALG_1:def 18;
then (x \ ((x \ y) \ y)) \ y in I by A2, Th51;
then A3: (x \ y) \ ((x \ y) \ y) in I by BCIALG_1:7;
assume (x \ y) \ y in A ; :: thesis: x \ y in A
hence x \ y in A by A1, A3, BCIALG_1:def 18; :: thesis: verum

end;

hence A is positive-implicative-ideal of X by Th51; :: thesis: verum