theorem Th3: :: ARYTM_1:3
for x, y, z being Element of REAL+ st x <=' y & y <=' z holds
x <=' z