set TR1 = TOP-REAL 1;
let A be Subset of (TOP-REAL 1); ( A is closed & A is bounded implies A is compact )
assume that
A1:
A is closed
and
A2:
A is bounded
; A is compact
consider r being Real such that
A3:
for q being Point of (TOP-REAL 1) st q in A holds
|.q.| < r
by A2, JORDAN2C:34;
reconsider L = [.(- r),r.] as Subset of R^1 by TOPMETR:17;
consider f being Function of (TOP-REAL 1),R^1 such that
A4:
for p being Element of (TOP-REAL 1) holds f . p = p /. 1
by JORDAN2B:1;
A5:
f is being_homeomorphism
by A4, JORDAN2B:28;
then reconsider F = f as one-to-one Function by TOPS_2:def 5;
rng f = [#] R^1
by A5, TOPS_2:def 5;
then
f is onto
by FUNCT_2:def 3;
then
f /" = F "
by TOPS_2:def 4;
then A6:
(f /") .: L = F " L
by FUNCT_1:85;
A7:
dom f = [#] (TOP-REAL 1)
by A5, TOPS_2:def 5;
A8:
A c= F " L
[.(- r),r.] is compact
by RCOMP_1:6;
then A14:
L is compact
by JORDAN5A:25;
f " is continuous
by A5, TOPS_2:def 5;
then
(f /") .: L is compact
by A14, WEIERSTR:8;
hence
A is compact
by A1, A6, A8, COMPTS_1:9; verum