theorem :: SRINGS_5:55

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