theorem :: XREAL_1:50

for a, b being Real st a < b holds
0 < b - a by Lm21;