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

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

hence
A is positive-implicative-ideal of X
by Th51; :: thesis: verum
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;((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