for r being Real holds rng (REAL --> r) c= REAL