reconsider x = x as Real by XREAL_0:def 1;
x in { g where g is Real : x <= g } ;
hence not right_closed_halfline x is empty by XXREAL_1:232; :: thesis: verum