theorem Th24: :: MESFUN16:24

for r being Real
for S being RealNormSpace
for E being Subset of S
for f being PartFunc of S,RNS_Real st f is_continuous_on E & dom f = E holds
ex H being Subset of S st
( H /\ E = f " ].-infty,r.[ & H is open )