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