let M be non empty MetrSpace; :: thesis: ( M is compact iff for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) )

thus ( M is compact implies for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) ) :: thesis: ( ( for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) ) implies M is compact )
proof
set TM = TopSpaceMetr M;
assume M is compact ; :: thesis: for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite )

then A1: TopSpaceMetr M is compact ;
let F be Subset-Family of M; :: thesis: ( F is being_ball-family & F is Cover of M implies ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) )

reconsider TF = F as Subset-Family of () ;
assume that
A2: F is being_ball-family and
A3: F is Cover of M ; :: thesis: ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite )

A4: TF is open
proof
let P be Subset of (); :: according to TOPS_2:def 1 :: thesis: ( not P in TF or P is open )
reconsider P9 = P as Subset of M ;
assume P in TF ; :: thesis: P is open
then ex p being Point of M ex r being Real st P9 = Ball (p,r) by A2;
hence P is open by Th14; :: thesis: verum
end;
the carrier of M c= union F by ;
then the carrier of () c= union TF ;
then TF is Cover of () by SETFAM_1:def 11;
then consider TG being Subset-Family of () such that
A5: TG c= TF and
A6: TG is Cover of () and
A7: TG is finite by ;
reconsider G = TG as Subset-Family of M ;
take G ; :: thesis: ( G c= F & G is Cover of M & G is finite )
the carrier of () c= union TG by ;
then the carrier of M c= union G ;
hence ( G c= F & G is Cover of M & G is finite ) by ; :: thesis: verum
end;
thus ( ( for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) ) implies M is compact ) :: thesis: verum
proof
set TM = TopSpaceMetr M;
assume A8: for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) ; :: thesis: M is compact
now :: thesis: for F being Subset-Family of () st F is Cover of () & F is open holds
ex GG being Subset-Family of () st
( GG c= F & GG is Cover of () & GG is finite )
let F be Subset-Family of (); :: thesis: ( F is Cover of () & F is open implies ex GG being Subset-Family of () st
( GG c= F & GG is Cover of () & GG is finite ) )

set Z = { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of () st
( P in F & Ball (p,r) c= P )
}
;
{ (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of () st
( P in F & Ball (p,r) c= P ) } c= bool the carrier of M
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of () st
( P in F & Ball (p,r) c= P )
}
or a in bool the carrier of M )

assume a in { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of () st
( P in F & Ball (p,r) c= P )
}
; :: thesis: a in bool the carrier of M
then ex p being Point of M ex r being Real st
( a = Ball (p,r) & ex P being Subset of () st
( P in F & Ball (p,r) c= P ) ) ;
hence a in bool the carrier of M ; :: thesis: verum
end;
then reconsider Z = { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of () st
( P in F & Ball (p,r) c= P )
}
as Subset-Family of M ;
assume that
A9: F is Cover of () and
A10: F is open ; :: thesis: ex GG being Subset-Family of () st
( GG c= F & GG is Cover of () & GG is finite )

the carrier of M c= union Z
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of M or a in union Z )
assume a in the carrier of M ; :: thesis: a in union Z
then reconsider p = a as Point of M ;
( the carrier of () c= union F & the carrier of () = the carrier of M ) by ;
then p in union F ;
then consider P being set such that
A11: p in P and
A12: P in F by TARSKI:def 4;
reconsider P = P as Subset of () by A12;
P is open by ;
then consider r being Real such that
A13: r > 0 and
A14: Ball (p,r) c= P by ;
reconsider r9 = r as Element of REAL by XREAL_0:def 1;
A15: a in Ball (p,r) by ;
Ball (p,r9) in Z by ;
hence a in union Z by ; :: thesis: verum
end;
then A16: Z is Cover of M by SETFAM_1:def 11;
reconsider F9 = F as non empty Subset-Family of () by ;
defpred S1[ object , object ] means ex D1, D2 being set st
( D1 = \$1 & D2 = \$2 & D1 c= D2 );
Z is being_ball-family
proof
let P be set ; :: according to TOPMETR:def 4 :: thesis: ( P in Z implies ex p being Point of M ex r being Real st P = Ball (p,r) )
assume P in Z ; :: thesis: ex p being Point of M ex r being Real st P = Ball (p,r)
then ex p being Point of M ex r being Real st
( P = Ball (p,r) & ex P being Subset of () st
( P in F & Ball (p,r) c= P ) ) ;
hence ex p being Point of M ex r being Real st P = Ball (p,r) ; :: thesis: verum
end;
then consider G being Subset-Family of M such that
A17: G c= Z and
A18: G is Cover of M and
A19: G is finite by ;
A20: for a being object st a in G holds
ex u being object st
( u in F9 & S1[a,u] )
proof
let a be object ; :: thesis: ( a in G implies ex u being object st
( u in F9 & S1[a,u] ) )

assume a in G ; :: thesis: ex u being object st
( u in F9 & S1[a,u] )

then a in Z by A17;
then consider p being Point of M, r being Real such that
A21: Ball (p,r) = a and
A22: ex P being Subset of () st
( P in F & Ball (p,r) c= P ) ;
consider P being Subset of () such that
A23: ( P in F & Ball (p,r) c= P ) by A22;
take P ; :: thesis: ( P in F9 & S1[a,P] )
thus ( P in F9 & S1[a,P] ) by ; :: thesis: verum
end;
consider f being Function of G,F9 such that
A24: for a being object st a in G holds
S1[a,f . a] from reconsider GG = rng f as Subset-Family of () by TOPS_2:2;
take GG = GG; :: thesis: ( GG c= F & GG is Cover of () & GG is finite )
thus GG c= F ; :: thesis: ( GG is Cover of () & GG is finite )
the carrier of () c= union GG
proof
A25: ( the carrier of () = the carrier of M & the carrier of M c= union G ) by ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of () or a in union GG )
assume a in the carrier of () ; :: thesis: a in union GG
then consider P being set such that
A26: a in P and
A27: P in G by ;
S1[P,f . P] by ;
then A28: P c= f . P ;
dom f = G by FUNCT_2:def 1;
then f . P in GG by ;
hence a in union GG by ; :: thesis: verum
end;
hence GG is Cover of () by SETFAM_1:def 11; :: thesis: GG is finite
dom f = G by FUNCT_2:def 1;
hence GG is finite by ; :: thesis: verum
end;
then TopSpaceMetr M is compact by COMPTS_1:def 1;
hence M is compact ; :: thesis: verum
end;