let a, b, c be Real; :: thesis: ( a <= b & c < a implies b -' a < b -' c )
assume that
A1: a <= b and
A2: c < a ; :: thesis: b -' a < b -' c
A3: b - a < b - c by A2, Th15;
b -' c = b - c by A1, A2, Th233, XXREAL_0:2;
hence b -' a < b -' c by A1, A3, Th48, XREAL_0:def 2; :: thesis: verum