theorem Th7: :: ARYTM_1:7

for x, y, z being Element of REAL+ holds
( x <=' y iff x + z <=' y + z )