let X be BCK-algebra; :: thesis: for I, A being Ideal of X st I c= A & I is commutative Ideal of X holds
A is commutative Ideal of X
let I, A be Ideal of X; :: thesis: ( I c= A & I is commutative Ideal of X implies A is commutative Ideal of X )
assume A1: ( I c= A & I is commutative Ideal of X ) ; :: thesis: A is commutative Ideal of X
for x, y being Element of X st x \ y in A holds
x \ (y \ (y \ x)) in A

proof

let x, y be Element of X; :: thesis: ( x \ y in A implies x \ (y \ (y \ x)) in A )
assume A2: x \ y in A ; :: thesis: x \ (y \ (y \ x)) in A
(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
then (x \ (x \ y)) \ y in I by BCIALG_1:def 18;
then (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in I by TL251, A1;
then (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in A by A1;
then (x \ (y \ (y \ (x \ (x \ y))))) \ (x \ y) in A by BCIALG_1:7;
then A5: x \ (y \ (y \ (x \ (x \ y)))) in A by A2, BCIALG_1:def 18;
(x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7
.= (x \ y) ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then A6: x \ (x \ y) <= x by BCIALG_1:def 11;
for x, y, z, u being Element of X st x <= y holds
u \ (z \ x) <= u \ (z \ y)

proof

let x, y, z, u be Element of X; :: thesis: ( x <= y implies u \ (z \ x) <= u \ (z \ y) )
assume x <= y ; :: thesis: u \ (z \ x) <= u \ (z \ y)
then z \ y <= z \ x by BCIALG_1:5;
hence u \ (z \ x) <= u \ (z \ y) by BCIALG_1:5; :: thesis: verum

end;

then y \ (y \ (x \ (x \ y))) <= y \ (y \ x) by A6;
then x \ (y \ (y \ x)) <= x \ (y \ (y \ (x \ (x \ y)))) by BCIALG_1:5;
hence x \ (y \ (y \ x)) in A by P141, A5; :: thesis: verum

end;

hence A is commutative Ideal of X by TL251; :: thesis: verum