theorem Th9: :: ARYTM_1:9

for x, y being Element of REAL+ holds
( x <=' y or x -' y <> {} )