theorem :: FCONT_3:25

for p being Real
for f being PartFunc of REAL,REAL st right_open_halfline p c= dom f & f | (right_open_halfline p) is continuous & ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) holds
rng (f | (right_open_halfline p)) is open