let X be BCK-algebra; :: thesis: ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )
thus ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) :: thesis: ( ( for x, y being Element of X holds x \ y = 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 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 A1, Def1 ;
hence x \ y = x \ (y \ (y \ x)) ; :: thesis: verum

end;

assume A2: for x, y being Element of X holds x \ y = 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 \ (y \ x))) <= y \ (y \ x) by Th2;
hence x \ (x \ y) <= y \ (y \ x) by A2; :: thesis: verum

end;

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