theorem :: SEQ_4:37

for seq being Real_Sequence st seq is bounded_above & seq is V47() holds
for n being Nat holds seq . n <= lim seq