theorem :: XREAL_1:49

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