theorem Th16: :: FCONT_2:16

for g, p being Real
for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )