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 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