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