theorem Th6: :: ARYTM_1:6

for x, y being Element of REAL+ st x = {} holds
x <=' y