theorem Th2: :: BCIALG_3:2

for X being BCK-algebra
for x, y being Element of X holds
( x \ (x \ y) <= y & x \ (x \ y) <= x )