deffunc H₁( 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 such that
A2: r > 0 and
A3: for p, q being Point of st p <> q & p in A & q in A holds
dist p,q >= r and
A4: not A is finite by Th31;
reconsider A = A as Subset of ;
set F = { {x} where x is Element of : x in A } ;
reconsider F = { {x} where x is Element of : x in A } as Subset-Family of by RELSET_2:16;

A5: now

let a be Subset of ; :: thesis: ( a in F implies card a = 1 )
assume a in F ; :: thesis: card a = 1
then ex y being Point of st
( a = {y} & y in A ) ;
hence card a = 1 by CARD_1:50; :: thesis: verum

end;

set PP = { H₁(y) where y is Subset of : y in F } ;
A6: A c= { H₁(y) where y is Subset of : y in F }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in { H₁(y) where y is Subset of : y in F } )
assume A7: y in A ; :: thesis: y in { H₁(y) where y is Subset of : y in F }
reconsider y' = y as Point of by A7;
{y'} in F by A7;
then H₁({y'}) in { H₁(y) where y is Subset of : y in F } ;
hence y in { H₁(y) where y is Subset of : y in F } by SETFAM_1:11; :: thesis: verum

end;

F is locally_finite by A2, A3, Lm7;
then A8: F is finite by A1, A5, Th27;
{ H₁(y) where y is Subset of : y in F } is finite from FRAENKEL:sch 21(A8);
hence contradiction by A4, A6; :: thesis: verum