theorem Th4: :: IDEA_1:4

for b1, b2, c being Nat st b2 <= c holds
b2 - b1 <= c