theorem :: INTEGRA8:35

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