let X be BCK-algebra; :: thesis: for x, y being Element of X holds
( x \ (x \ y) <= y & x \ (x \ y) <= x )
let x, y be Element of X; :: thesis: ( x \ (x \ y) <= y & x \ (x \ y) <= x )
A1: (x \ (x \ y)) \ y = 0. X by BCIALG_1:1;
A2: ((x \ (x \ y)) \ ((0. X) \ (x \ y))) \ (x \ (0. X)) = 0. X by BCIALG_1:def 3;
(0. X) \ (x \ y) = (x \ y) `
.= 0. X by BCIALG_1:def 8 ;
then ((x \ (x \ y)) \ (0. X)) \ x = 0. X by A2, BCIALG_1:2;
then (x \ (x \ y)) \ x = 0. X by BCIALG_1:2;
hence ( x \ (x \ y) <= y & x \ (x \ y) <= x ) by A1, BCIALG_1:def 11; :: thesis: verum