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

per cases ;

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

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();
A3: R is open

for A being Subset of R^1 st A in R holds
A is open

let A be Subset of R^1 ; :: thesis:
assume A in R ; :: thesis:
then consider x being Point of RealSpace such that
A4: ( x in [#] P & A = Ball x,1 ) by A2;
thus A is open by A4, TOPMETR:21, TOPMETR:def 7; :: thesis:

end;

hence R is open by TOPS_2:def 1; :: thesis:

end;

[#] P c= union R

for x being set st x in [#] P holds
x in union R

let x be set ; :: thesis:
assume A5: x in [#] P ; :: thesis:
then reconsider x = x as Point of RealSpace by METRIC_1:def 14;
consider A being Subset of RealSpace such that
A6: 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 )

A7: dist x,x = 0 by METRIC_1:1;
take A ; :: thesis:
thus ( x in A & A in R ) by A2, A5, A6, A7, METRIC_1:12; :: thesis:

end;

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

end;

hence [#] P c= union R by TARSKI:def 3; :: thesis:

end;

then R is Cover of P by SETFAM_1:def 12;
then consider R0 being Subset-Family of R^1 such that
A8: ( R0 c= R & R0 is Cover of P & R0 is finite ) by A1, A3, COMPTS_1:def 7;
A9: P c= union R0 by A8, 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

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

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 )

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

end;

A18: [#] P is bounded_above