theorem Th11: :: ARYTM_1:11

for x, y being Element of REAL+ holds x -' y <=' x