let P be Subset of R^1 ; :: thesis: ( P is compact implies [#] P is bounded )
assume A1: P is compact ; :: thesis: [#] P is bounded
thus [#] P is bounded :: thesis: verum

proof

now

per cases ( [#] P <> {} or [#] P = {} ) ;

case [#] P <> {} ; :: thesis: [#] P is bounded

set r0 = 1;
defpred S₁[ Subset of R^1 ] means ex x being Point of RealSpace st
( x in [#] P & $1 = Ball x,1 );
consider R being Subset-Family of R^1 such that
A2: for A being Subset of R^1 holds
( A in R iff S₁[A] ) from SUBSET_1:sch 3();
for x being set st x in [#] P holds
x in union R

proof

let x be set ; :: thesis: ( x in [#] P implies x in union R )
assume A3: x in [#] P ; :: thesis: x in union R
then reconsider x = x as Point of RealSpace by METRIC_1:def 14;
consider A being Subset of RealSpace such that
A4: A = Ball x,1 ;
R^1 = TopStruct(# the carrier of RealSpace ,(Family_open_set RealSpace ) #) by PCOMPS_1:def 6, TOPMETR:def 7;
then reconsider A = A as Subset of R^1 ;
ex A being set st
( x in A & A in R )

proof

take A ; :: thesis: ( x in A & A in R )
dist x,x = 0 by METRIC_1:1;
hence ( x in A & A in R ) by A2, A3, A4, METRIC_1:12; :: thesis: verum

end;

hence x in union R by TARSKI:def 4; :: thesis: verum

end;

then [#] P c= union R by TARSKI:def 3;
then A5: R is Cover of P by SETFAM_1:def 12;
for A being Subset of R^1 st A in R holds
A is open

proof

let A be Subset of R^1 ; :: thesis: ( A in R implies A is open )
assume A in R ; :: thesis: A is open
then ex x being Point of RealSpace st
( x in [#] P & A = Ball x,1 ) by A2;
hence A is open by TOPMETR:21, TOPMETR:def 7; :: thesis: verum

end;

then R is open by TOPS_2:def 1;
then consider R0 being Subset-Family of R^1 such that
A6: R0 c= R and
A7: R0 is Cover of P and
A8: R0 is finite by A1, A5, COMPTS_1:def 7;
A9: P c= union R0 by A7, SETFAM_1:def 12;
A10: for A being set st A in R0 holds
ex x being Point of RealSpace ex r being Real st A = Ball x,r

proof

let A be set ; :: thesis: ( A in R0 implies ex x being Point of RealSpace ex r being Real st A = Ball x,r )
assume A11: A in R0 ; :: thesis: ex x being Point of RealSpace ex r being Real st A = Ball x,r
then reconsider A = A as Subset of R^1 ;
consider x being Point of RealSpace such that
x in [#] P and
A12: A = Ball x,1 by A2, A6, A11;
take x ; :: thesis: ex r being Real st A = Ball x,r
take 1 ; :: thesis: A = Ball x,1
thus A = Ball x,1 by A12; :: thesis: verum

end;

R^1 = TopStruct(# the carrier of RealSpace ,(Family_open_set RealSpace ) #) by PCOMPS_1:def 6, TOPMETR:def 7;
then reconsider R0 = R0 as Subset-Family of RealSpace ;
R0 is being_ball-family by A10, TOPMETR:def 4;
then consider x1 being Point of RealSpace such that
A13: ex r1 being Real st union R0 c= Ball x1,r1 by A8, Th3;
consider r1 being Real such that
A14: union R0 c= Ball x1,r1 by A13;
A15: [#] P c= Ball x1,r1 by A9, A14, XBOOLE_1:1;
reconsider x1 = x1 as Real by METRIC_1:def 14;
A16: for p being Real st p in [#] P holds
( x1 - r1 <= p & p <= x1 + r1 )

proof

let p be Real; :: thesis: ( p in [#] P implies ( x1 - r1 <= p & p <= x1 + r1 ) )
reconsider a = x1, b = p as Element of RealSpace by METRIC_1:def 14;
assume p in [#] P ; :: thesis: ( x1 - r1 <= p & p <= x1 + r1 )
then dist a,b < r1 by A15, METRIC_1:12;
then A17: abs (x1 - p) < r1 by TOPMETR:15;
then - r1 <= x1 - p by ABSVALUE:12;
then (- r1) + p <= x1 by XREAL_1:21;
then A18: p <= x1 - (- r1) by XREAL_1:21;
x1 - p <= r1 by A17, ABSVALUE:12;
then x1 <= p + r1 by XREAL_1:22;
hence ( x1 - r1 <= p & p <= x1 + r1 ) by A18, XREAL_1:22; :: thesis: verum

end;

x1 - r1 is LowerBound of [#] P

proof

let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in [#] P or x1 - r1 <= r )
thus ( not r in [#] P or x1 - r1 <= r ) by A16; :: thesis: verum

end;

then A19: [#] P is bounded_below by XXREAL_2:def 9;
x1 + r1 is UpperBound of [#] P

proof

let r be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not r in [#] P or r <= x1 + r1 )
thus ( not r in [#] P or r <= x1 + r1 ) by A16; :: thesis: verum

end;

then [#] P is bounded_above by XXREAL_2:def 10;
hence [#] P is bounded by A19, XXREAL_2:def 11; :: thesis: verum

end;

case A20: [#] P = {} ; :: thesis: [#] P is bounded

0 is LowerBound of [#] P

proof

let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in [#] P or 0 <= r )
thus ( not r in [#] P or 0 <= r ) by A20; :: thesis: verum

end;

then A21: [#] P is bounded_below by XXREAL_2:def 9;
0 is UpperBound of [#] P

proof

let r be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not r in [#] P or r <= 0 )
thus ( not r in [#] P or r <= 0 ) by A20; :: thesis: verum

end;

then [#] P is bounded_above by XXREAL_2:def 10;
hence [#] P is bounded by A21, XXREAL_2:def 11; :: thesis: verum

end;

end;

end;

hence [#] P is bounded ; :: thesis: verum

end;