theorem Th2: :: MESFUNC5:2

for x, y being R_eal holds y - x <= |.(x - y).|