theorem :: NUMBER09:59

for k, n being Nat st k > 0 holds
not n in GreaterOrEqualsNumbers (n + k)