let X be BCK-algebra; :: thesis: ( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra )

A1: ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )

then for x, y being Element of X st x \ y in {(0. X)} holds

x \ (y \ (y \ x)) in {(0. X)} by A1;

hence {(0. X)} is commutative Ideal of X by Th33, BCIALG_1:43; :: thesis: verum

A1: ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )

proof

thus
( {(0. X)} is commutative Ideal of X implies X is commutative BCK-algebra )
:: thesis: ( X is commutative BCK-algebra implies {(0. X)} is commutative Ideal of X )
assume A2:
X is commutative BCK-algebra
; :: thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x))

let x, y be Element of X; :: thesis: x \ y = x \ (y \ (y \ x))

x \ y = x \ (x \ (x \ y)) by BCIALG_1:8

.= x \ (y \ (y \ x)) by A2, BCIALG_3:def 1 ;

hence x \ y = x \ (y \ (y \ x)) ; :: thesis: verum

end;let x, y be Element of X; :: thesis: x \ y = x \ (y \ (y \ x))

x \ y = x \ (x \ (x \ y)) by BCIALG_1:8

.= x \ (y \ (y \ x)) by A2, BCIALG_3:def 1 ;

hence x \ y = x \ (y \ (y \ x)) ; :: thesis: verum

proof

assume
X is commutative BCK-algebra
; :: thesis: {(0. X)} is commutative Ideal of X
assume A3:
{(0. X)} is commutative Ideal of X
; :: thesis: X is commutative BCK-algebra

for x, y being Element of X st x <= y holds

x = y \ (y \ x)

end;for x, y being Element of X st x <= y holds

x = y \ (y \ x)

proof

hence
X is commutative BCK-algebra
by BCIALG_3:5; :: thesis: verum
let x, y be Element of X; :: thesis: ( x <= y implies x = y \ (y \ x) )

assume x <= y ; :: thesis: x = y \ (y \ x)

then x \ y = 0. X ;

then x \ y in {(0. X)} by TARSKI:def 1;

then x \ (y \ (y \ x)) in {(0. X)} by A3, Th33;

then ( (y \ (y \ x)) \ x = 0. X & x \ (y \ (y \ x)) = 0. X ) by BCIALG_1:1, TARSKI:def 1;

hence x = y \ (y \ x) by BCIALG_1:def 7; :: thesis: verum

end;assume x <= y ; :: thesis: x = y \ (y \ x)

then x \ y = 0. X ;

then x \ y in {(0. X)} by TARSKI:def 1;

then x \ (y \ (y \ x)) in {(0. X)} by A3, Th33;

then ( (y \ (y \ x)) \ x = 0. X & x \ (y \ (y \ x)) = 0. X ) by BCIALG_1:1, TARSKI:def 1;

hence x = y \ (y \ x) by BCIALG_1:def 7; :: thesis: verum

then for x, y being Element of X st x \ y in {(0. X)} holds

x \ (y \ (y \ x)) in {(0. X)} by A1;

hence {(0. X)} is commutative Ideal of X by Th33, BCIALG_1:43; :: thesis: verum