theorem Th48: :: XREAL_1:48

for a, b being Real st a <= b holds
0 <= b - a