theorem Th27: :: SRINGS_5:31

the_set_of_all_right_open_real_bounded_intervals c= { I where I is Subset of REAL : I is right_open_interval }