theorem :: BCIALG_4:15

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