let X be BCK-algebra; :: thesis: ( X is commutative BCK-algebra implies for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x )
assume A1: X is commutative BCK-algebra ; :: thesis: for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x
let x, y, a be Element of X; :: thesis: ( y <= a implies (a \ x) \ (a \ y) = y \ x )
assume y <= a ; :: thesis: (a \ x) \ (a \ y) = y \ x
then A2: y \ a = 0. X ;
(a \ x) \ (a \ y) = (a \ (a \ y)) \ x by BCIALG_1:7
.= (y \ (0. X)) \ x by A1, A2, Def1
.= y \ x by BCIALG_1:2 ;
hence (a \ x) \ (a \ y) = y \ x ; :: thesis: verum