1 in { g where g is Real : 0 < g } ;
hence not right_open_halfline 0 is empty by XXREAL_1:230; :: thesis: verum