theorem :: SRINGS_5:56
( the_set_of_all_closed_real_bounded_intervals is cap-closed & the_set_of_all_closed_real_bounded_intervals is with_empty_element & the_set_of_all_closed_real_bounded_intervals is with_countable_Cover )