theorem :: XREAL_1:47

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