{r} c= REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {r} or x in REAL )
assume x in {r} ; :: thesis: x in REAL
hence x in REAL by XREAL_0:def 1; :: thesis: verum

end;

hence {r} is Subset of REAL ; :: thesis: verum