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 )

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

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

thus
( ( for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
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 (TopSpaceMetr M) ;

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

then the carrier of (TopSpaceMetr M) c= union TF ;

then TF is Cover of (TopSpaceMetr M) by SETFAM_1:def 11;

then consider TG being Subset-Family of (TopSpaceMetr M) such that

A5: TG c= TF and

A6: TG is Cover of (TopSpaceMetr M) and

A7: TG is finite by A1, A4, COMPTS_1:def 1;

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 (TopSpaceMetr M) c= union TG by A6, SETFAM_1:def 11;

then the carrier of M c= union G ;

hence ( G c= F & G is Cover of M & G is finite ) by A5, A7, SETFAM_1:def 11; :: thesis: verum

end;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 (TopSpaceMetr M) ;

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

the carrier of M c= union F
by A3, SETFAM_1:def 11;
let P be Subset of (TopSpaceMetr M); :: 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;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

then the carrier of (TopSpaceMetr M) c= union TF ;

then TF is Cover of (TopSpaceMetr M) by SETFAM_1:def 11;

then consider TG being Subset-Family of (TopSpaceMetr M) such that

A5: TG c= TF and

A6: TG is Cover of (TopSpaceMetr M) and

A7: TG is finite by A1, A4, COMPTS_1:def 1;

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 (TopSpaceMetr M) c= union TG by A6, SETFAM_1:def 11;

then the carrier of M c= union G ;

hence ( G c= F & G is Cover of M & G is finite ) by A5, A7, SETFAM_1:def 11; :: thesis: verum

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

hence M is compact ; :: thesis: verum

end;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 (TopSpaceMetr M) st F is Cover of (TopSpaceMetr M) & F is open holds

ex GG being Subset-Family of (TopSpaceMetr M) st

( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )

then
TopSpaceMetr M is compact
by COMPTS_1:def 1;ex GG being Subset-Family of (TopSpaceMetr M) st

( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )

let F be Subset-Family of (TopSpaceMetr M); :: thesis: ( F is Cover of (TopSpaceMetr M) & F is open implies ex GG being Subset-Family of (TopSpaceMetr M) st

( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite ) )

set Z = { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) 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 (TopSpaceMetr M) st

( P in F & Ball (p,r) c= P ) } c= bool the carrier of M

( P in F & Ball (p,r) c= P ) } as Subset-Family of M ;

assume that

A9: F is Cover of (TopSpaceMetr M) and

A10: F is open ; :: thesis: ex GG being Subset-Family of (TopSpaceMetr M) st

( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )

the carrier of M c= union Z

reconsider F9 = F as non empty Subset-Family of (TopSpaceMetr M) by A9, TOPS_2:3;

defpred S_{1}[ object , object ] means ex D1, D2 being set st

( D1 = $1 & D2 = $2 & D1 c= D2 );

Z is being_ball-family

A17: G c= Z and

A18: G is Cover of M and

A19: G is finite by A8, A16;

A20: for a being object st a in G holds

ex u being object st

( u in F9 & S_{1}[a,u] )

A24: for a being object st a in G holds

S_{1}[a,f . a]
from FUNCT_2:sch 1(A20);

reconsider GG = rng f as Subset-Family of (TopSpaceMetr M) by TOPS_2:2;

take GG = GG; :: thesis: ( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )

thus GG c= F ; :: thesis: ( GG is Cover of (TopSpaceMetr M) & GG is finite )

the carrier of (TopSpaceMetr M) c= union GG

dom f = G by FUNCT_2:def 1;

hence GG is finite by A19, FINSET_1:8; :: thesis: verum

end;( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite ) )

set Z = { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) 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 (TopSpaceMetr M) st

( P in F & Ball (p,r) c= P ) } c= bool the carrier of M

proof

then reconsider Z = { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) st
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 (TopSpaceMetr M) 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 (TopSpaceMetr M) 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 (TopSpaceMetr M) st

( P in F & Ball (p,r) c= P ) ) ;

hence a in bool the carrier of M ; :: thesis: verum

end;( 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 (TopSpaceMetr M) 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 (TopSpaceMetr M) st

( P in F & Ball (p,r) c= P ) ) ;

hence a in bool the carrier of M ; :: thesis: verum

( P in F & Ball (p,r) c= P ) } as Subset-Family of M ;

assume that

A9: F is Cover of (TopSpaceMetr M) and

A10: F is open ; :: thesis: ex GG being Subset-Family of (TopSpaceMetr M) st

( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )

the carrier of M c= union Z

proof

then A16:
Z is Cover of M
by SETFAM_1:def 11;
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 (TopSpaceMetr M) c= union F & the carrier of (TopSpaceMetr M) = the carrier of M ) by A9, SETFAM_1:def 11;

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 (TopSpaceMetr M) by A12;

P is open by A10, A12;

then consider r being Real such that

A13: r > 0 and

A14: Ball (p,r) c= P by A11, Th15;

reconsider r9 = r as Element of REAL by XREAL_0:def 1;

A15: a in Ball (p,r) by A13, TBSP_1:11;

Ball (p,r9) in Z by A12, A14;

hence a in union Z by A15, TARSKI:def 4; :: thesis: verum

end;assume a in the carrier of M ; :: thesis: a in union Z

then reconsider p = a as Point of M ;

( the carrier of (TopSpaceMetr M) c= union F & the carrier of (TopSpaceMetr M) = the carrier of M ) by A9, SETFAM_1:def 11;

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 (TopSpaceMetr M) by A12;

P is open by A10, A12;

then consider r being Real such that

A13: r > 0 and

A14: Ball (p,r) c= P by A11, Th15;

reconsider r9 = r as Element of REAL by XREAL_0:def 1;

A15: a in Ball (p,r) by A13, TBSP_1:11;

Ball (p,r9) in Z by A12, A14;

hence a in union Z by A15, TARSKI:def 4; :: thesis: verum

reconsider F9 = F as non empty Subset-Family of (TopSpaceMetr M) by A9, TOPS_2:3;

defpred S

( D1 = $1 & D2 = $2 & D1 c= D2 );

Z is being_ball-family

proof

then consider G being Subset-Family of M such that
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 (TopSpaceMetr M) 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;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 (TopSpaceMetr M) 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

A17: G c= Z and

A18: G is Cover of M and

A19: G is finite by A8, A16;

A20: for a being object st a in G holds

ex u being object st

( u in F9 & S

proof

consider f being Function of G,F9 such that
let a be object ; :: thesis: ( a in G implies ex u being object st

( u in F9 & S_{1}[a,u] ) )

assume a in G ; :: thesis: ex u being object st

( u in F9 & S_{1}[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 (TopSpaceMetr M) st

( P in F & Ball (p,r) c= P ) ;

consider P being Subset of (TopSpaceMetr M) such that

A23: ( P in F & Ball (p,r) c= P ) by A22;

take P ; :: thesis: ( P in F9 & S_{1}[a,P] )

thus ( P in F9 & S_{1}[a,P] )
by A21, A23; :: thesis: verum

end;( u in F9 & S

assume a in G ; :: thesis: ex u being object st

( u in F9 & S

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 (TopSpaceMetr M) st

( P in F & Ball (p,r) c= P ) ;

consider P being Subset of (TopSpaceMetr M) such that

A23: ( P in F & Ball (p,r) c= P ) by A22;

take P ; :: thesis: ( P in F9 & S

thus ( P in F9 & S

A24: for a being object st a in G holds

S

reconsider GG = rng f as Subset-Family of (TopSpaceMetr M) by TOPS_2:2;

take GG = GG; :: thesis: ( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )

thus GG c= F ; :: thesis: ( GG is Cover of (TopSpaceMetr M) & GG is finite )

the carrier of (TopSpaceMetr M) c= union GG

proof

hence
GG is Cover of (TopSpaceMetr M)
by SETFAM_1:def 11; :: thesis: GG is finite
A25:
( the carrier of (TopSpaceMetr M) = the carrier of M & the carrier of M c= union G )
by A18, SETFAM_1:def 11;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (TopSpaceMetr M) or a in union GG )

assume a in the carrier of (TopSpaceMetr M) ; :: thesis: a in union GG

then consider P being set such that

A26: a in P and

A27: P in G by A25, TARSKI:def 4;

S_{1}[P,f . P]
by A24, A27;

then A28: P c= f . P ;

dom f = G by FUNCT_2:def 1;

then f . P in GG by A27, FUNCT_1:def 3;

hence a in union GG by A26, A28, TARSKI:def 4; :: thesis: verum

end;let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (TopSpaceMetr M) or a in union GG )

assume a in the carrier of (TopSpaceMetr M) ; :: thesis: a in union GG

then consider P being set such that

A26: a in P and

A27: P in G by A25, TARSKI:def 4;

S

then A28: P c= f . P ;

dom f = G by FUNCT_2:def 1;

then f . P in GG by A27, FUNCT_1:def 3;

hence a in union GG by A26, A28, TARSKI:def 4; :: thesis: verum

dom f = G by FUNCT_2:def 1;

hence GG is finite by A19, FINSET_1:8; :: thesis: verum

hence M is compact ; :: thesis: verum