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 )

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

( 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 A3:
for x, y being Element of X st x \ y in I holds
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 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

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

hence
I is commutative Ideal of X
by Def6; :: thesis: verum
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;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