theorem :: BCIALG_4:16

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