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