let T be non empty TopSpace; :: thesis: ( T is compact implies T is pseudocompact )
assume A1: T is compact ; :: thesis: T is pseudocompact
let f be RealMap of T; :: according to PSCOMP_1:def 27 :: thesis: ( f is continuous implies f is bounded )
assume A2: f is continuous ; :: thesis: f is bounded
thus f is bounded_above :: according to SEQ_2:def 8 :: thesis: f is bounded_below

proof

consider p being Element of T;
defpred S₁[ Real] means c₁ >= f . p;
set R = { (right_closed_halfline r3) where r3 is Real : S₁[r3] } ;
A3: { (right_closed_halfline r3) where r3 is Real : S₁[r3] } is Subset-Family of REAL from DOMAIN_1:sch 8();
A4: right_closed_halfline (f . p) in { (right_closed_halfline r3) where r3 is Real : S₁[r3] } ;
then reconsider R = { (right_closed_halfline r3) where r3 is Real : S₁[r3] } as non empty Subset-Family of REAL by A3;
reconsider F = (" f) .: R as Subset-Family of T ;
A5: F is c=-linear

proof

let X, Y be set ; :: according to ORDINAL1:def 9 :: thesis: ( not X in F or not Y in F or X,Y are_c=-comparable )
assume X in F ; :: thesis: ( not Y in F or X,Y are_c=-comparable )
then consider A being set such that
A6: A in bool REAL and
A7: A in R and
A8: X = (" f) . A by FUNCT_2:115;
A9: X = f " A by A6, A8, MEASURE6:def 7;
consider r1 being Real such that
A10: A = right_closed_halfline r1 and
r1 >= f . p by A7;
assume Y in F ; :: thesis: X,Y are_c=-comparable
then consider B being set such that
A11: B in bool REAL and
A12: B in R and
A13: Y = (" f) . B by FUNCT_2:115;
A14: Y = f " B by A11, A13, MEASURE6:def 7;
consider r2 being Real such that
A15: B = right_closed_halfline r2 and
r2 >= f . p by A12;
( r1 >= r2 or r2 >= r1 ) ;
then ( X c= Y or Y c= X ) by A10, A15, A9, A14, RELAT_1:178, XXREAL_1:38;
hence X,Y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

assume A16: for s being real number holds s is not UpperBound of f .: the carrier of T ; :: according to XXREAL_2:def 10,MEASURE6:def 15 :: thesis: contradiction

now

assume {} in F ; :: thesis: contradiction
then consider rchx being set such that
A17: rchx in bool REAL and
A18: rchx in R and
A19: {} = (" f) . rchx by FUNCT_2:115;
consider r3 being Real such that
A20: rchx = right_closed_halfline r3 and
r3 >= f . p by A18;
r3 is not UpperBound of f .: the carrier of T by A16;
then consider r1 being ext-real number such that
A21: r1 in f .: the carrier of T and
A22: r1 > r3 by XXREAL_2:def 1;
rchx = { g where g is Real : g >= r3 } by A20, XXREAL_1:232;
then A23: r1 in rchx by A21, A22;
A24: ex c being set st
( c in the carrier of T & c in the carrier of T & r1 = f . c ) by A21, FUNCT_2:115;
{} = f " rchx by A17, A19, MEASURE6:def 7;
hence contradiction by A24, A23, FUNCT_2:46; :: thesis: verum

end;

then A25: F is with_non-empty_elements by SETFAM_1:def 9;
R is closed

proof

let X be Subset of REAL ; :: according to MEASURE6:def 11 :: thesis: ( not X in R or X is closed )
assume X in R ; :: thesis: X is closed
then ex r3 being Real st
( X = right_closed_halfline r3 & r3 >= f . p ) ;
hence X is closed ; :: thesis: verum

end;

then A26: F is closed by A2, Th59;
(" f) . (right_closed_halfline (f . p)) in F by A4, FUNCT_2:43;
then meet F <> {} by A1, A25, A5, A26, COMPTS_1:13;
then consider x being set such that
A27: x in meet F by XBOOLE_0:def 1;
consider eR being Element of R;
eR in R ;
then consider er being Real such that
A28: eR = right_closed_halfline er and
A29: er >= f . p ;
reconsider x = x as Element of T by A27;
A30: f . x in meet R by A27, MEASURE6:71;
then A31: f . x in eR by SETFAM_1:def 1;
consider fx9 being real number such that
A32: fx9 > f . x by XREAL_1:3;
reconsider fx9 = fx9 as Real by XREAL_0:def 1;
right_closed_halfline er = { r3 where r3 is Real : r3 >= er } by XXREAL_1:232;
then ex r1 being Real st
( f . x = r1 & r1 >= er ) by A31, A28;
then f . x >= f . p by A29, XXREAL_0:2;
then fx9 >= f . p by A32, XXREAL_0:2;
then right_closed_halfline fx9 in R ;
then A33: f . x in right_closed_halfline fx9 by A30, SETFAM_1:def 1;
right_closed_halfline fx9 = { r3 where r3 is Real : r3 >= fx9 } by XXREAL_1:232;
then ex r3 being Real st
( f . x = r3 & r3 >= fx9 ) by A33;
hence contradiction by A32; :: thesis: verum

end;

consider p being Element of T;
defpred S₁[ Real] means c₁ <= f . p;
set R = { (left_closed_halfline r3) where r3 is Real : S₁[r3] } ;
A34: { (left_closed_halfline r3) where r3 is Real : S₁[r3] } is Subset-Family of REAL from DOMAIN_1:sch 8();
A35: left_closed_halfline (f . p) in { (left_closed_halfline r3) where r3 is Real : S₁[r3] } ;
then reconsider R = { (left_closed_halfline r3) where r3 is Real : S₁[r3] } as non empty Subset-Family of REAL by A34;
reconsider F = (" f) .: R as Subset-Family of T ;
R is closed

proof

let X be Subset of REAL ; :: according to MEASURE6:def 11 :: thesis: ( not X in R or X is closed )
assume X in R ; :: thesis: X is closed
then ex r3 being Real st
( X = left_closed_halfline r3 & r3 <= f . p ) ;
hence X is closed ; :: thesis: verum

end;

then A36: F is closed by A2, Th59;
A37: F is c=-linear

proof

let X, Y be set ; :: according to ORDINAL1:def 9 :: thesis: ( not X in F or not Y in F or X,Y are_c=-comparable )
assume X in F ; :: thesis: ( not Y in F or X,Y are_c=-comparable )
then consider A being set such that
A38: A in bool REAL and
A39: A in R and
A40: X = (" f) . A by FUNCT_2:115;
A41: X = f " A by A38, A40, MEASURE6:def 7;
consider r1 being Real such that
A42: A = left_closed_halfline r1 and
r1 <= f . p by A39;
assume Y in F ; :: thesis: X,Y are_c=-comparable
then consider B being set such that
A43: B in bool REAL and
A44: B in R and
A45: Y = (" f) . B by FUNCT_2:115;
A46: Y = f " B by A43, A45, MEASURE6:def 7;
consider r2 being Real such that
A47: B = left_closed_halfline r2 and
r2 <= f . p by A44;
( r1 <= r2 or r2 <= r1 ) ;
then ( X c= Y or Y c= X ) by A42, A47, A41, A46, RELAT_1:178, XXREAL_1:42;
hence X,Y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

assume A48: for s being real number holds s is not LowerBound of f .: the carrier of T ; :: according to XXREAL_2:def 9,MEASURE6:def 14 :: thesis: contradiction

now

assume {} in F ; :: thesis: contradiction
then consider rchx being set such that
A49: rchx in bool REAL and
A50: rchx in R and
A51: {} = (" f) . rchx by FUNCT_2:115;
consider r3 being Real such that
A52: rchx = left_closed_halfline r3 and
r3 <= f . p by A50;
r3 is not LowerBound of f .: the carrier of T by A48;
then consider r1 being ext-real number such that
A53: r1 in f .: the carrier of T and
A54: r1 < r3 by XXREAL_2:def 2;
rchx = { g where g is Real : g <= r3 } by A52, XXREAL_1:231;
then A55: r1 in rchx by A53, A54;
A56: ex c being set st
( c in the carrier of T & c in the carrier of T & r1 = f . c ) by A53, FUNCT_2:115;
{} = f " rchx by A49, A51, MEASURE6:def 7;
hence contradiction by A56, A55, FUNCT_2:46; :: thesis: verum

end;

then A57: F is with_non-empty_elements by SETFAM_1:def 9;
(" f) . (left_closed_halfline (f . p)) in F by A35, FUNCT_2:43;
then meet F <> {} by A1, A57, A37, A36, COMPTS_1:13;
then consider x being set such that
A58: x in meet F by XBOOLE_0:def 1;
consider eR being Element of R;
eR in R ;
then consider er being Real such that
A59: eR = left_closed_halfline er and
A60: er <= f . p ;
reconsider x = x as Element of T by A58;
A61: f . x in meet R by A58, MEASURE6:71;
then A62: f . x in eR by SETFAM_1:def 1;
consider fx9 being real number such that
A63: fx9 < f . x by XREAL_1:4;
reconsider fx9 = fx9 as Real by XREAL_0:def 1;
left_closed_halfline er = { r3 where r3 is Real : r3 <= er } by XXREAL_1:231;
then ex r1 being Real st
( f . x = r1 & r1 <= er ) by A62, A59;
then f . x <= f . p by A60, XXREAL_0:2;
then fx9 <= f . p by A63, XXREAL_0:2;
then left_closed_halfline fx9 in R ;
then A64: f . x in left_closed_halfline fx9 by A61, SETFAM_1:def 1;
left_closed_halfline fx9 = { r3 where r3 is Real : r3 <= fx9 } by XXREAL_1:231;
then ex r3 being Real st
( f . x = r3 & r3 <= fx9 ) by A64;
hence contradiction by A63; :: thesis: verum