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

(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