theorem :: SRINGS_5:53
for n being Nat holds (Seg n) --> the_set_of_all_closed_real_bounded_intervals is b1 -element FinSequence