Description: Plus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021)
|- -. +oo e. RR
|- +oo e/ RR