theorem Th7: :: BCIALG_4:8

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 )