let P be Subset of R^1; :: thesis: ( P is compact implies [#] P is closed )
assume A1: P is compact ; :: thesis: [#] P is closed

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

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

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

A3: R^1 is T_2 by PCOMPS_1:34, TOPMETR:def 6;
for s1 being Real_Sequence st rng s1 c= [#] P & s1 is convergent holds
lim s1 in [#] P

proof

let s1 be Real_Sequence; :: thesis: ( rng s1 c= [#] P & s1 is convergent implies lim s1 in [#] P )
assume that
A4: rng s1 c= [#] P and
A5: s1 is convergent ; :: thesis: lim s1 in [#] P
set x = lim s1;
lim s1 in REAL by XREAL_0:def 1;
then reconsider x = lim s1 as Point of R^1 by TOPMETR:17;
thus lim s1 in [#] P :: thesis: verum

proof

assume not lim s1 in [#] P ; :: thesis: contradiction
then x in P ` by SUBSET_1:29;
then consider Otx, OtP being Subset of R^1 such that
A6: Otx is open and
OtP is open and
A7: x in Otx and
A8: ( P c= OtP & Otx misses OtP ) by A1, A2, A3, COMPTS_1:6;
A9: R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) by PCOMPS_1:def 5, TOPMETR:def 6;
then reconsider x = x as Point of RealSpace ;
consider r being Real such that
A10: r > 0 and
A11: Ball (x,r) c= Otx by A6, A7, TOPMETR:15, TOPMETR:def 6;
reconsider r = r as Real ;
A12: Ball (x,r) = { q where q is Element of RealSpace : dist (x,q) < r } by METRIC_1:17;
rng s1 misses Otx by A4, A8, XBOOLE_1:1, XBOOLE_1:63;
then A13: Ball (x,r) misses rng s1 by A11, XBOOLE_1:63;
for n being Nat ex m being Nat st
( n <= m & not |.((s1 . m) - (lim s1)).| < r )

proof

given n being Nat such that A14: for m being Nat st n <= m holds
|.((s1 . m) - (lim s1)).| < r ; :: thesis: contradiction
set m = n + 1;
reconsider ls = lim s1 as Element of REAL by XREAL_0:def 1;
|.((s1 . (n + 1)) - ls).| < r by A14, NAT_1:11;
then real_dist . ((s1 . (n + 1)),ls) < r by METRIC_1:def 12;
then A15: real_dist . (ls,(s1 . (n + 1))) < r by METRIC_1:9;
reconsider y = s1 . (n + 1) as Element of RealSpace by A9, TOPMETR:17;
A16: s1 . (n + 1) in rng s1 by FUNCT_2:4;
dist (x,y) = the distance of RealSpace . (x,y) by METRIC_1:def 1;
then y in Ball (x,r) by A12, A15, METRIC_1:def 13;
then y in (Ball (x,r)) /\ (rng s1) by A16, XBOOLE_0:def 4;
hence contradiction by A13, XBOOLE_0:def 7; :: thesis: verum

end;

hence contradiction by A5, A10, SEQ_2:def 7; :: thesis: verum

end;

end;

hence [#] P is closed by RCOMP_1:def 4; :: thesis: verum

end;

case A17: [#] P = {} ; :: thesis: [#] P is closed

for s1 being Real_Sequence st rng s1 c= [#] P & s1 is convergent holds
lim s1 in [#] P

proof

let s1 be Real_Sequence; :: thesis: ( rng s1 c= [#] P & s1 is convergent implies lim s1 in [#] P )
assume that
A18: rng s1 c= [#] P and
s1 is convergent ; :: thesis: lim s1 in [#] P
0 in NAT ;
hence lim s1 in [#] P by A17, A18, FUNCT_2:4; :: thesis: verum

end;

hence [#] P is closed by RCOMP_1:def 4; :: thesis: verum

end;

end;

end;

hence [#] P is closed ; :: thesis: verum