Description: The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021)
|- RR =/= (/)
|- 0 e. RR