let M be non empty MetrSpace; :: thesis: ( TopSpaceMetr M is compact iff TopSpaceMetr M is countably_compact )
set T = TopSpaceMetr M;
thus ( TopSpaceMetr M is compact implies TopSpaceMetr M is countably_compact ) by Th20; :: thesis: ( TopSpaceMetr M is countably_compact implies TopSpaceMetr M is compact )
assume A1: TopSpaceMetr M is countably_compact ; :: thesis: TopSpaceMetr M is compact
then M is totally_bounded by Th32;
then A2: TopSpaceMetr M is second-countable by Th33;
let F be Subset-Family of (TopSpaceMetr M); :: according to COMPTS_1:def 3 :: thesis: ( not F is Cover of the carrier of (TopSpaceMetr M) or not F is open or ex b₁ being Element of bool (bool the carrier of (TopSpaceMetr M)) st
( b₁ c= F & b₁ is Cover of the carrier of (TopSpaceMetr M) & b₁ is finite ) )
assume A3: ( F is Cover of (TopSpaceMetr M) & F is open ) ; :: thesis: ex b₁ being Element of bool (bool the carrier of (TopSpaceMetr M)) st
( b₁ c= F & b₁ is Cover of the carrier of (TopSpaceMetr M) & b₁ is finite )
consider G being Subset-Family of (TopSpaceMetr M) such that
A4: ( G c= F & G is Cover of (TopSpaceMetr M) & G is countable ) by A2, A3, Th34;
G is open by A3, A4, TOPS_2:18;
then consider H being Subset-Family of (TopSpaceMetr M) such that
A5: ( H c= G & H is Cover of (TopSpaceMetr M) & H is finite ) by A1, A4, Def9;
thus ex b₁ being Element of bool (bool the carrier of (TopSpaceMetr M)) st
( b₁ c= F & b₁ is Cover of the carrier of (TopSpaceMetr M) & b₁ is finite ) by A4, A5, XBOOLE_1:1; :: thesis: verum