set TR1 = TOP-REAL 1;
let A be Subset of (TOP-REAL 1); :: thesis: ( A is closed & A is bounded implies A is compact )
assume that
A1: A is closed and
A2: A is bounded ; :: thesis: 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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in F " L )
assume A9: x in A ; :: thesis: x in F " L
then reconsider v = x as Element of (TOP-REAL 1) ;
set v1 = v . 1;
A10: len v = 1 by CARD_1:def 7;
then v = <*(v . 1)*> by FINSEQ_1:40;
then A11: |.v.| = |.(v . 1).| by TOPREALC:18;
|.v.| < r by A3, A9;
then ( v . 1 <= r & - r <= v . 1 ) by A11, ABSVALUE:5;
then A12: v . 1 in L by XXREAL_1:1;
( 1 in Seg 1 & dom v = Seg 1 ) by A10, FINSEQ_1:1, FINSEQ_1:def 3;
then A13: v /. 1 = v . 1 by PARTFUN1:def 6;
f . v = v /. 1 by A4;
hence x in F " L by A7, A12, A13, FUNCT_1:def 7; :: thesis: verum
end;
[.(- 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; :: thesis: verum