:: deftheorem defines the_set_of_all_left_open_real_bounded_intervals SRINGS_5:def 7 :
the_set_of_all_left_open_real_bounded_intervals = { ].a,b.] where a, b is Real : verum } ;