theorem :: NUMBER09:60

for n being Nat
for k being b₁ _or_greater Nat holds k in GreaterOrEqualsNumbers n by EC_PF_2:def 1, Th56;