theorem Th30: :: FCONT_1:30

for f being PartFunc of REAL,REAL st dom f <> {} & dom f is compact & f | (dom f) is continuous holds
ex x1, x2 being Real st
( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) )