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

x in { g where g is Real : x <= g } ;

hence not right_closed_halfline x is empty by XXREAL_1:232; :: thesis: verum