theorem :: SRINGS_5:55

the_set_of_all_closed_real_bounded_intervals = { I where I is Subset of REAL : I is closed_interval }