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 that
A1: I c= A and
A2: 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 )
A3: 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;

(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 x \ (x \ y) <= x ;
then y \ (y \ (x \ (x \ y))) <= y \ (y \ x) by A3;
then A4: x \ (y \ (y \ x)) <= x \ (y \ (y \ (x \ (x \ y)))) by BCIALG_1:5;
(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 A2, Th33;
then (x \ (x \ y)) \ (y \ (y \ (x \ (x \ y)))) in A by A1;
then A5: (x \ (y \ (y \ (x \ (x \ y))))) \ (x \ y) in A by BCIALG_1:7;
assume x \ y in A ; :: thesis: x \ (y \ (y \ x)) in A
then x \ (y \ (y \ (x \ (x \ y)))) in A by A5, BCIALG_1:def 18;
hence x \ (y \ (y \ x)) in A by A4, Th5; :: thesis: verum

end;

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