Description: The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020)
|- RR+ e. _V
|- RR e. _V
|- RR+ C_ RR