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