theorem :: BCIALG_4:40

for X being BCK-Algebra_with_Condition(S)
for x, y being Element of X holds (x \ y) * (y \ x) <= x * y