deffunc H1( set ) -> set = meet $1;
let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: ( TopSpaceMetr M is countably_compact implies M is totally_bounded )
assume A1: TopSpaceMetr M is countably_compact ; :: thesis: M is totally_bounded
set T = TopSpaceMetr M;
assume not M is totally_bounded ; :: thesis: contradiction
then consider r being Real, A being Subset of M such that
A2: r > 0 and
A3: for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r and
A4: A is infinite by Th30;
reconsider A = A as Subset of (TopSpaceMetr M) ;
set F = { {x} where x is Element of (TopSpaceMetr M) : x in A } ;
reconsider F = { {x} where x is Element of (TopSpaceMetr M) : x in A } as Subset-Family of (TopSpaceMetr M) by RELSET_2:16;
A5: now :: thesis: for a being Subset of (TopSpaceMetr M) st a in F holds
card a = 1
let a be Subset of (TopSpaceMetr M); :: thesis: ( a in F implies card a = 1 )
assume a in F ; :: thesis: card a = 1
then ex y being Point of (TopSpaceMetr M) st
( a = {y} & y in A ) ;
hence card a = 1 by CARD_1:30; :: thesis: verum
end;
set PP = { H1(y) where y is Subset of (TopSpaceMetr M) : y in F } ;
A6: A c= { H1(y) where y is Subset of (TopSpaceMetr M) : y in F }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in { H1(y) where y is Subset of (TopSpaceMetr M) : y in F } )
assume A7: y in A ; :: thesis: y in { H1(y) where y is Subset of (TopSpaceMetr M) : y in F }
reconsider y9 = y as Point of (TopSpaceMetr M) by A7;
{y9} in F by A7;
then H1({y9}) in { H1(y) where y is Subset of (TopSpaceMetr M) : y in F } ;
hence y in { H1(y) where y is Subset of (TopSpaceMetr M) : y in F } by SETFAM_1:10; :: thesis: verum
end;
F is locally_finite by A2, A3, Lm7;
then A8: F is finite by A1, A5, Th26;
{ H1(y) where y is Subset of (TopSpaceMetr M) : y in F } is finite from FRAENKEL:sch 21(A8);
 hence contradiction by A4, A6; :: thesis: verum