theorem Th50: :: NAT_D:50
for i, i1, i2 being natural Number st i >= i1 holds
i >= i1 -' i2