let a, b, c be Real; :: thesis: ( a <= b - c implies c <= b - a )
assume a <= b - c ; :: thesis: c <= b - a
then a + c <= b by Lm17;
hence c <= b - a by Lm16; :: thesis: verum