theorem :: NUMBER09:57

for k, n being Nat holds n + k in GreaterOrEqualsNumbers n by Th56, NAT_1:11;