].0,0.] in the_set_of_all_left_open_real_bounded_intervals ;
hence not the_set_of_all_left_open_real_bounded_intervals is empty ; :: thesis: verum