( [.0,0.[ in the_set_of_all_right_open_real_bounded_intervals & [.0,0.[ = {} ) ;
hence the_set_of_all_right_open_real_bounded_intervals is with_empty_element ; :: thesis: verum