let X be BCK-algebra; :: thesis: ( X is commutative BCK-algebra implies for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) )
assume A1: X is commutative BCK-algebra ; :: thesis: for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y )
let x, y be Element of X; :: thesis: ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y )
A2: (x \ y) \ ((x \ y) \ x) = x \ (x \ (x \ y)) by A1, Def1
.= x \ y by BCIALG_1:8 ;
x \ (y \ (y \ x)) = x \ (x \ (x \ y)) by A1, Def1
.= x \ y by BCIALG_1:8 ;
hence ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by A2; :: thesis: verum