theorem Th29: :: RINFSUP1:29

for seq being Real_Sequence
for n being Nat holds { (seq . k) where k is Nat : n <= k } is Subset of REAL