theorem :: WSIERP_1:18

for a, b, c being Nat st a <= b - c holds
( a <= b & c <= b )