theorem :: SRINGS_5:30

the_set_of_all_left_open_real_bounded_intervals is Semiring of REAL by Th26, SRINGS_3:10;