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

now

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

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

[#] P is bounded by A1, Th17;
hence [#] P is compact by A1, Th18, RCOMP_1:29; :: thesis: verum

end;

case A2: [#] P = {} ; :: thesis: ( not [#] P is compact implies [#] P is compact )

assume not [#] P is compact ; :: thesis: [#] P is compact
then consider s1 being Real_Sequence such that
A3: ( rng s1 c= [#] P & ( for s2 being Real_Sequence holds
( not s2 is subsequence of s1 or not s2 is convergent or not lim s2 in [#] P ) ) ) by RCOMP_1:def 3;
consider x being set such that
A4: x in NAT by XBOOLE_0:def 1;
s1 . x in rng s1 by A4, FUNCT_2:6;
hence [#] P is compact by A2, A3; :: thesis: verum

end;

end;

end;

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