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

proof

assume A1: X is commutative BCK-algebra ; :: thesis: for x, y being Element of X st x <= y holds
x = y \ (y \ x)
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 y \ (y \ x) = x \ (0. X) by A1, Def1
.= x by BCIALG_1:2 ;
hence x = y \ (y \ x) ; :: thesis: verum

end;

assume A2: for x, y being Element of X st x <= y holds
x = y \ (y \ x) ; :: thesis: X is commutative BCK-algebra
for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x)

proof

let x, y be Element of X; :: thesis: x \ (x \ y) <= y \ (y \ x)
(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 A3: y \ x <= 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 ;
then x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2;
hence x \ (x \ y) <= y \ (y \ x) by A3, BCIALG_1:5; :: thesis: verum

end;

hence X is commutative BCK-algebra by Th1; :: thesis: verum