theorem :: SRINGS_5:53

for n being Nat holds (Seg n) --> the_set_of_all_closed_real_bounded_intervals is b₁ -element FinSequence