theorem Th3: :: IDEA_1:3

for a, b being Nat holds a - b <= a