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

proof

let x, y be Element of X; :: thesis: ( x \ y in I implies x \ (y \ (y \ x)) in I )
assume B1: x \ y in I ; :: thesis: x \ (y \ (y \ x)) in I
(x \ (y \ (y \ x))) \ x = (x \ x) \ (y \ (y \ x)) by BCIALG_1:7
.= (y \ (y \ x)) ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then x \ (y \ (y \ x)) <= x by BCIALG_1:def 11;
then y \ x <= y \ (x \ (y \ (y \ x))) by BCIALG_1:5;
then (x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x)))) <= (x \ (y \ (y \ x))) \ (y \ x) by BCIALG_1:5;
then B2: ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) <= ((x \ (y \ (y \ x))) \ (y \ x)) \ (x \ y) by BCIALG_1:5;
(x \ (y \ (y \ x))) \ (y \ x) = (x \ (y \ x)) \ (y \ (y \ x)) by BCIALG_1:7;
then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) <= 0. X by B2, BCIALG_1:def 3;
then (((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y)) \ (0. X) = 0. X by BCIALG_1:def 11;
then ((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) = 0. X by BCIALG_1:2;
then (x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x)))) <= x \ y by BCIALG_1:def 11;
hence x \ (y \ (y \ x)) in I by P351, A, B1, P141; :: thesis: verum

end;

for x, y being Element of X st (x \ y) \ y in I holds
x \ y in I

proof

let x, y be Element of X; :: thesis: ( (x \ y) \ y in I implies x \ y in I )
assume A1: (x \ y) \ y in I ; :: thesis: x \ y in I
((x \ y) \ (x \ (x \ y))) \ ((x \ y) \ y) = 0. X by BCIALG_1:1;
then (x \ y) \ (x \ (x \ y)) <= (x \ y) \ y by BCIALG_1:def 11;
hence x \ y in I by A, P351, P141, A1; :: thesis: verum

end;

hence ( I is commutative Ideal of X & I is positive-implicative-ideal of X ) by C1, TL251, TL341; :: thesis: verum