let T be non empty TopSpace; :: thesis: for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
let f be Function of T,R^1 ; :: thesis: for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
let P be Subset of T; :: thesis: ( P <> {} & P is compact & f is continuous implies ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) )
assume A1: ( P <> {} & P is compact & f is continuous ) ; :: thesis: ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
A2: [#] (f .: P) <> {}

proof

A3: dom f = the carrier of T by FUNCT_2:def 1;
consider x being set such that
A4: x in P by A1, XBOOLE_0:def 1;
f . x in f .: P by A3, A4, FUNCT_1:def 12;
hence [#] (f .: P) <> {} ; :: thesis: verum

end;

consider y1, y2 being Real such that
A5: y1 = upper_bound ([#] (f .: P)) and
A6: y2 = lower_bound ([#] (f .: P)) ;
[#] (f .: P) is compact by A1, Th14, Th19;
then A7: ( y1 in [#] (f .: P) & y2 in [#] (f .: P) ) by A2, A5, A6, RCOMP_1:32;
then consider x1 being set such that
A8: ( x1 in dom f & x1 in P & y1 = f . x1 ) by FUNCT_1:def 12;
consider x2 being set such that
A9: ( x2 in dom f & x2 in P & y2 = f . x2 ) by A7, FUNCT_1:def 12;
reconsider x1 = x1, x2 = x2 as Point of T by A8, A9;
take x1 ; :: thesis: ex x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
take x2 ; :: thesis: ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
thus ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) by A5, A6, A8, A9; :: thesis: verum