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 x2 being Point of T st

( x2 in 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 x2 being Point of T st

( x2 in P & f . x2 = lower_bound (f .: P) )

let P be Subset of T; :: thesis: ( P <> {} & P is compact & f is continuous implies ex x2 being Point of T st

( x2 in P & f . x2 = lower_bound (f .: P) ) )

assume ( P <> {} & P is compact & f is continuous ) ; :: thesis: ex x2 being Point of T st

( x2 in P & f . x2 = lower_bound (f .: P) )

then consider x1, x2 being Point of T such that

x1 in P and

A1: x2 in P and

f . x1 = upper_bound ([#] (f .: P)) and

A2: f . x2 = lower_bound ([#] (f .: P)) by Lm1;

take x2 ; :: thesis: ( x2 in P & f . x2 = lower_bound (f .: P) )

thus ( x2 in P & f . x2 = lower_bound (f .: P) ) by A1, A2; :: thesis: verum

for P being Subset of T st P <> {} & P is compact & f is continuous holds

ex x2 being Point of T st

( x2 in 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 x2 being Point of T st

( x2 in P & f . x2 = lower_bound (f .: P) )

let P be Subset of T; :: thesis: ( P <> {} & P is compact & f is continuous implies ex x2 being Point of T st

( x2 in P & f . x2 = lower_bound (f .: P) ) )

assume ( P <> {} & P is compact & f is continuous ) ; :: thesis: ex x2 being Point of T st

( x2 in P & f . x2 = lower_bound (f .: P) )

then consider x1, x2 being Point of T such that

x1 in P and

A1: x2 in P and

f . x1 = upper_bound ([#] (f .: P)) and

A2: f . x2 = lower_bound ([#] (f .: P)) by Lm1;

take x2 ; :: thesis: ( x2 in P & f . x2 = lower_bound (f .: P) )

thus ( x2 in P & f . x2 = lower_bound (f .: P) ) by A1, A2; :: thesis: verum