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