theorem :: NUMBER09:58

for n being Nat holds n in GreaterOrEqualsNumbers n by Th56;