theorem Th5: :: ARYTM_1:5

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