for i, i1, i2 being natural Number st i >= i1 holds
i >= i1 -' i2