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

proof

now :: thesis: ( ( [#] P <> {} & [#] P is real-bounded ) or ( [#] P = {} & [#] P is real-bounded ) )

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

case [#] P <> {} ; :: thesis: [#] P is real-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 object st x in [#] P holds
x in union R

proof

let x be object ; :: 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 13;
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 5, TOPMETR:def 6;
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:11; :: thesis: verum

end;

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

end;

then [#] P c= union R ;
then A5: R is Cover of P by SETFAM_1:def 11;
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:14, TOPMETR:def 6; :: 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 4;
A9: P c= union R0 by A7, SETFAM_1:def 11;
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 5, TOPMETR:def 6;
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;
reconsider x1 = x1 as Element of REAL by METRIC_1:def 13;
A16: for p being Element of REAL st p in [#] P holds
( x1 - r1 <= p & p <= x1 + r1 )

proof

let p be Element of 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 13;
assume p in [#] P ; :: thesis: ( x1 - r1 <= p & p <= x1 + r1 )
then dist (a,b) < r1 by A15, METRIC_1:11;
then A17: |.(x1 - p).| < r1 by TOPMETR:11;
then - r1 <= x1 - p by ABSVALUE:5;
then (- r1) + p <= x1 by XREAL_1:19;
then A18: p <= x1 - (- r1) by XREAL_1:19;
x1 - p <= r1 by A17, ABSVALUE:5;
then x1 <= p + r1 by XREAL_1:20;
hence ( x1 - r1 <= p & p <= x1 + r1 ) by A18, XREAL_1:20; :: thesis: verum

end;

x1 - r1 is LowerBound of [#] P

proof

let r be ExtReal; :: 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 ;
x1 + r1 is UpperBound of [#] P

proof

let r be ExtReal; :: 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 ;
hence [#] P is real-bounded by A19; :: thesis: verum

end;

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

0 is LowerBound of [#] P

proof

let r be ExtReal; :: 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 ;
0 is UpperBound of [#] P

proof

let r be ExtReal; :: 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 ;
hence [#] P is real-bounded by A21; :: thesis: verum

end;

end;

end;

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

end;