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 ) ; :: thesis: ( TopSpaceMetr M is countably_compact implies TopSpaceMetr M is compact )
assume A1: TopSpaceMetr M is countably_compact ; :: thesis: TopSpaceMetr M is compact
let F be Subset-Family of (TopSpaceMetr M); :: according to COMPTS_1:def 1 :: 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 that
A2: F is Cover of (TopSpaceMetr M) and
A3: 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 )
M is totally_bounded by A1, Th31;
then TopSpaceMetr M is second-countable by Th32;
then consider G being Subset-Family of (TopSpaceMetr M) such that
A4: G c= F and
A5: G is Cover of (TopSpaceMetr M) and
A6: G is countable by A2, A3, Th33;
G is open by A3, A4;
then ex H being Subset-Family of (TopSpaceMetr M) st
( H c= G & H is Cover of (TopSpaceMetr M) & H is finite ) by A1, A5, A6;
hence 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, XBOOLE_1:1; :: thesis: verum