let X be BCK-algebra; :: thesis: for I being Ideal of X holds
( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I )
let I be Ideal of X; :: thesis: ( I is commutative Ideal of X iff for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I )
thus ( I is commutative Ideal of X implies for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I ) :: thesis: ( ( for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I ) implies I is commutative Ideal of X )

proof

A1: 0. X in I by BCIALG_1:def 18;
assume A2: I is commutative Ideal of X ; :: thesis: for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I
let x, y be Element of X; :: thesis: ( x \ y in I implies x \ (y \ (y \ x)) in I )
assume x \ y in I ; :: thesis: x \ (y \ (y \ x)) in I
then (x \ y) \ (0. X) in I by BCIALG_1:2;
hence x \ (y \ (y \ x)) in I by A2, A1, Def6; :: thesis: verum

end;

assume A3: for x, y being Element of X st x \ y in I holds
x \ (y \ (y \ x)) in I ; :: thesis: I is commutative Ideal of X
for x, y, z being Element of X st (x \ y) \ z in I & z in I holds
x \ (y \ (y \ x)) in I

proof

let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in I & z in I implies x \ (y \ (y \ x)) in I )
assume ( (x \ y) \ z in I & z in I ) ; :: thesis: x \ (y \ (y \ x)) in I
then x \ y in I by BCIALG_1:def 18;
hence x \ (y \ (y \ x)) in I by A3; :: thesis: verum

end;

hence I is commutative Ideal of X by Def6; :: thesis: verum