theorem Th8: :: ARYTM_1:8

for x, y, z being Element of REAL+ st x <=' y holds
x *' z <=' y *' z