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 :: thesis: ( ( [#] P <> {} & [#] P is compact ) or ( [#] P = {} & ( not [#] P is compact implies [#] P is compact ) ) )

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

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

[#] P is real-bounded by A1, Th11;
hence [#] P is compact by A1, Th12, RCOMP_1:11; :: 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 A3: ex s1 being Real_Sequence st
( 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;
0 in NAT ;
hence [#] P is compact by A2, A3, FUNCT_2:4; :: thesis: verum

end;

end;

end;

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