let P be Subset of R^1; ( P is compact implies [#] P is real-bounded )
assume A1:
P is compact
; [#] P is real-bounded
thus
[#] P is real-bounded
verumproof
now ( ( [#] P <> {} & [#] P is real-bounded ) or ( [#] P = {} & [#] P is real-bounded ) )per cases
( [#] P <> {} or [#] P = {} )
;
case
[#] P <> {}
;
[#] P is real-bounded set r0 = 1;
defpred S1[
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
S1[
A] )
from SUBSET_1:sch 3();
for
x being
object st
x in [#] P holds
x in union R
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
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)
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 )
x1 - r1 is
LowerBound of
[#] P
then A19:
[#] P is
bounded_below
;
x1 + r1 is
UpperBound of
[#] P
then
[#] P is
bounded_above
;
hence
[#] P is
real-bounded
by A19;
verum end; end; end;
hence
[#] P is
real-bounded
;
verum
end;