let a, b, c be Nat; :: thesis: ( a <= b - c implies ( a <= b & c <= b ) )
assume a <= b - c ; :: thesis: ( a <= b & c <= b )
then a + c <= b by XREAL_1:19;
hence ( a <= b & c <= b ) by Lm7; :: thesis: verum