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

assume A1: 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 A2: x \ y in I ; :: thesis: x \ (y \ (y \ x)) in I
A3: (x \ y) \ (0. X) in I by A2, BCIALG_1:2;
0. X in I by BCIALG_1:def 18;
hence x \ (y \ (y \ x)) in I by A1, A3, Def4; :: thesis: verum

end;

assume A: 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 A2: ( (x \ y) \ z in I & z in I ) ; :: thesis: x \ (y \ (y \ x)) in I
x \ y in I by A2, BCIALG_1:def 18;
hence x \ (y \ (y \ x)) in I by A; :: thesis: verum

end;

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