{r} c= REAL by XREAL_0:def 1;
hence {r} is Subset of REAL ; :: thesis: verum