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 being Point of T st
( x1 in P & f . x1 = upper_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 being Point of T st
( x1 in P & f . x1 = upper_bound (f .: P) )
let P be Subset of T; :: thesis: ( P <> {} & P is compact & f is continuous implies ex x1 being Point of T st
( x1 in P & f . x1 = upper_bound (f .: P) ) )
assume ( P <> {} & P is compact & f is continuous ) ; :: thesis: ex x1 being Point of T st
( x1 in P & f . x1 = upper_bound (f .: P) )
then consider x1, x2 being Point of T such that
A1: x1 in P and
x2 in P and
A2: f . x1 = upper_bound ([#] (f .: P)) and
f . x2 = lower_bound ([#] (f .: P)) by Lm1;
take x1 ; :: thesis: ( x1 in P & f . x1 = upper_bound (f .: P) )
thus ( x1 in P & f . x1 = upper_bound (f .: P) ) by A1, A2; :: thesis: verum