let T be non empty TopSpace; :: thesis: ( ( for f being RealMap of T st f is continuous holds
f is bounded ) iff for f being RealMap of T st f is continuous holds
f is with_max )
set cT = the carrier of T;

hereby :: thesis: ( ( for f being RealMap of T st f is continuous holds
f is with_max ) implies for f being RealMap of T st f is continuous holds
f is bounded )

assume A1: for f being RealMap of T st f is continuous holds
f is bounded ; :: thesis: for f being RealMap of T st f is continuous holds
f is with_max
let f be RealMap of T; :: thesis: ( f is continuous implies f is with_max )
assume A2: f is continuous ; :: thesis: f is with_max
set fcT = f .: the carrier of T;
f is bounded by A1, A2;
then f is bounded_above ;
then A3: f .: the carrier of T is bounded_above by Def12;
assume not f is with_max ; :: thesis: contradiction
then A4: not f .: the carrier of T is with_max by Def14;
then A5: not sup (f .: the carrier of T) in f .: the carrier of T by A3, Def3;
set b = upper_bound (f .: the carrier of T);
set bf = (upper_bound (f .: the carrier of T)) + (- f);
set g = Inv ((upper_bound (f .: the carrier of T)) + (- f));
reconsider f' = f as Function of the carrier of T,REAL ;
reconsider bf' = (upper_bound (f .: the carrier of T)) + (- f) as Function of the carrier of T,REAL ;

A6: now

assume 0 in rng ((upper_bound (f .: the carrier of T)) + (- f)) ; :: thesis: contradiction
then consider x being set such that
A7: x in dom ((upper_bound (f .: the carrier of T)) + (- f)) and
A8: ((upper_bound (f .: the carrier of T)) + (- f)) . x = 0 by FUNCT_1:def 5;
reconsider x = x as Element of the carrier of T by A7;
bf' . x = (upper_bound (f .: the carrier of T)) + ((- f') . x) by VALUED_1:2
.= (upper_bound (f .: the carrier of T)) + (- (f . x)) by VALUED_1:8
.= (upper_bound (f .: the carrier of T)) - (f . x) ;
hence contradiction by A5, A8, FUNCT_2:43; :: thesis: verum

end;

set gcT = (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T;
- f is continuous by A2, Th55;
then (upper_bound (f .: the carrier of T)) + (- f) is continuous by Th56;
then A9: Inv ((upper_bound (f .: the carrier of T)) + (- f)) is continuous by A6, Th57;

now

Inv ((upper_bound (f .: the carrier of T)) + (- f)) is bounded by A1, A9;
then Inv ((upper_bound (f .: the carrier of T)) + (- f)) is bounded_above ;
then (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T is bounded_above by Def12;
then consider p being real number such that
A10: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p by SEQ_4:def 1;

per cases ( p <= 0 or p > 0 ) ;

suppose A11: p <= 0 ; :: thesis: ex 1' being real number st
( 1' > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= 1' ) )

reconsider 1' = 1 as real number ;
take 1' = 1'; :: thesis: ( 1' > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= 1' ) )
thus 1' > 0 ; :: thesis: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= 1'
let r be real number ; :: thesis: ( r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T implies r <= 1' )
assume r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T ; :: thesis: r <= 1'
hence r <= 1' by A10, A11; :: thesis: verum

end;

suppose A12: p > 0 ; :: thesis: ex p being real number st
( p > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ) )

take p = p; :: thesis: ( p > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ) )
thus p > 0 by A12; :: thesis: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p
thus for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p by A10; :: thesis: verum

end;

end;

end;

then consider p being real number such that
A13: p > 0 and
A14: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ;
1 / p > 0 by A13;
then consider r being real number such that
A15: r in f .: the carrier of T and
A16: (upper_bound (f .: the carrier of T)) - (1 / p) < r by A3, SEQ_4:def 4;
consider x being set such that
A17: ( x in the carrier of T & x in the carrier of T ) and
A18: r = f . x by A15, FUNCT_2:115;
reconsider x = x as Element of T by A17;
( f . x <= upper_bound (f .: the carrier of T) & f . x <> upper_bound (f .: the carrier of T) ) by A3, A4, A15, A18, Def3, SEQ_4:def 4;
then (f . x) + 0 < upper_bound (f .: the carrier of T) by XXREAL_0:1;
then A19: (upper_bound (f .: the carrier of T)) - (f . x) > 0 by XREAL_1:22;
(Inv ((upper_bound (f .: the carrier of T)) + (- f))) . x = (bf' . x) " by VALUED_1:10
.= ((upper_bound (f .: the carrier of T)) + ((- f') . x)) " by VALUED_1:2
.= 1 / ((upper_bound (f .: the carrier of T)) + ((- f') . x))
.= 1 / ((upper_bound (f .: the carrier of T)) + (- (f . x))) by VALUED_1:8
.= 1 / ((upper_bound (f .: the carrier of T)) - (f . x)) ;
then 1 / ((upper_bound (f .: the carrier of T)) - (f . x)) <= p by A14, FUNCT_2:43;
then 1 <= p * ((upper_bound (f .: the carrier of T)) - (f . x)) by A19, XREAL_1:83;
then 1 / p <= (upper_bound (f .: the carrier of T)) - (f . x) by A13, XREAL_1:81;
then (f . x) + (1 / p) <= upper_bound (f .: the carrier of T) by XREAL_1:21;
hence contradiction by A16, A18, XREAL_1:21; :: thesis: verum

end;

assume A20: for f being RealMap of T st f is continuous holds
f is with_max ; :: thesis: for f being RealMap of T st f is continuous holds
f is bounded
let f be RealMap of T; :: thesis: ( f is continuous implies f is bounded )
assume A21: f is continuous ; :: thesis: f is bounded
then f is with_max by A20;
then f .: the carrier of T is with_max by Def14;
then f .: the carrier of T is bounded_above by Def3;
hence f is bounded_above by Def12; :: according to SEQ_2:def 8 :: thesis: f is bounded_below
f is with_min by A20, A21, Th60;
then f .: the carrier of T is with_min by Def15;
then f .: the carrier of T is bounded_below by Def4;
hence f is bounded_below by Def11; :: thesis: verum