let M be MetrSpace; :: thesis: for F being Subset-Family of M st F is finite & F is being_ball-family holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

let F be Subset-Family of M; :: thesis: ( F is finite & F is being_ball-family implies ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume that

A1: F is finite and

A2: F is being_ball-family ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r)

consider p being FinSequence such that

A3: rng p = F by A1, FINSEQ_1:52;

A4: for F being Subset-Family of M st F is finite & F is being_ball-family holds

for n being Nat

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

hence ex x being Point of M ex r being Real st union F c= Ball (x,r) by A2, A4, A3; :: thesis: verum

ex x being Point of M ex r being Real st union F c= Ball (x,r)

let F be Subset-Family of M; :: thesis: ( F is finite & F is being_ball-family implies ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume that

A1: F is finite and

A2: F is being_ball-family ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r)

consider p being FinSequence such that

A3: rng p = F by A1, FINSEQ_1:52;

A4: for F being Subset-Family of M st F is finite & F is being_ball-family holds

for n being Nat

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

proof

ex n being Nat st dom p = Seg n
by FINSEQ_1:def 2;
defpred S_{1}[ Nat] means for F being Subset-Family of M st F is finite & F is being_ball-family holds

for n being Nat st n = $1 holds

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r);

A5: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A17, A5);

hence for F being Subset-Family of M st F is finite & F is being_ball-family holds

for n being Nat

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) ; :: thesis: verum

end;for n being Nat st n = $1 holds

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r);

A5: for k being Nat st S

S

proof

A17:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let F be Subset-Family of M; :: thesis: ( F is finite & F is being_ball-family implies for n being Nat st n = k + 1 holds

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume that

F is finite and

A7: F is being_ball-family ; :: thesis: for n being Nat st n = k + 1 holds

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

let n be Nat; :: thesis: ( n = k + 1 implies for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume A8: n = k + 1 ; :: thesis: for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

let p be FinSequence; :: thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume ( rng p = F & dom p = Seg n ) ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r)

then consider F1 being Subset-Family of M such that

A9: ( F1 is finite & F1 is being_ball-family ) and

A10: ex p1 being FinSequence st

( rng p1 = F1 & dom p1 = Seg k & ex x2 being Point of M ex r2 being Real st union F c= (union F1) \/ (Ball (x2,r2)) ) by A7, A8, Th2;

consider x1 being Point of M such that

A11: ex r being Real st union F1 c= Ball (x1,r) by A6, A9, A10;

consider x2 being Point of M such that

A12: ex r2 being Real st union F c= (union F1) \/ (Ball (x2,r2)) by A10;

consider r2 being Real such that

A13: union F c= (union F1) \/ (Ball (x2,r2)) by A12;

consider r1 being Real such that

A14: union F1 c= Ball (x1,r1) by A11;

consider x being Point of M such that

A15: ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by Th1;

take x ; :: thesis: ex r being Real st union F c= Ball (x,r)

consider r being Real such that

A16: (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by A15;

reconsider r = r as Real ;

take r ; :: thesis: union F c= Ball (x,r)

(union F1) \/ (Ball (x2,r2)) c= (Ball (x1,r1)) \/ (Ball (x2,r2)) by A14, XBOOLE_1:9;

then union F c= (Ball (x1,r1)) \/ (Ball (x2,r2)) by A13;

hence union F c= Ball (x,r) by A16; :: thesis: verum

end;assume A6: S

let F be Subset-Family of M; :: thesis: ( F is finite & F is being_ball-family implies for n being Nat st n = k + 1 holds

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume that

F is finite and

A7: F is being_ball-family ; :: thesis: for n being Nat st n = k + 1 holds

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

let n be Nat; :: thesis: ( n = k + 1 implies for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume A8: n = k + 1 ; :: thesis: for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

let p be FinSequence; :: thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume ( rng p = F & dom p = Seg n ) ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r)

then consider F1 being Subset-Family of M such that

A9: ( F1 is finite & F1 is being_ball-family ) and

A10: ex p1 being FinSequence st

( rng p1 = F1 & dom p1 = Seg k & ex x2 being Point of M ex r2 being Real st union F c= (union F1) \/ (Ball (x2,r2)) ) by A7, A8, Th2;

consider x1 being Point of M such that

A11: ex r being Real st union F1 c= Ball (x1,r) by A6, A9, A10;

consider x2 being Point of M such that

A12: ex r2 being Real st union F c= (union F1) \/ (Ball (x2,r2)) by A10;

consider r2 being Real such that

A13: union F c= (union F1) \/ (Ball (x2,r2)) by A12;

consider r1 being Real such that

A14: union F1 c= Ball (x1,r1) by A11;

consider x being Point of M such that

A15: ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by Th1;

take x ; :: thesis: ex r being Real st union F c= Ball (x,r)

consider r being Real such that

A16: (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by A15;

reconsider r = r as Real ;

take r ; :: thesis: union F c= Ball (x,r)

(union F1) \/ (Ball (x2,r2)) c= (Ball (x1,r1)) \/ (Ball (x2,r2)) by A14, XBOOLE_1:9;

then union F c= (Ball (x1,r1)) \/ (Ball (x2,r2)) by A13;

hence union F c= Ball (x,r) by A16; :: thesis: verum

proof

for n being Nat holds S
let F be Subset-Family of M; :: thesis: ( F is finite & F is being_ball-family implies for n being Nat st n = 0 holds

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume that

F is finite and

F is being_ball-family ; :: thesis: for n being Nat st n = 0 holds

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

let n be Nat; :: thesis: ( n = 0 implies for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume n = 0 ; :: thesis: for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

then A18: Seg n = {} ;

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

ex x being Point of M ex r being Real st union F c= Ball (x,r) ; :: thesis: verum

end;for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume that

F is finite and

F is being_ball-family ; :: thesis: for n being Nat st n = 0 holds

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

let n be Nat; :: thesis: ( n = 0 implies for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume n = 0 ; :: thesis: for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

then A18: Seg n = {} ;

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r)

proof

hence
for p being FinSequence st rng p = F & dom p = Seg n holds
set x = the Point of M;

let p be FinSequence; :: thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume A19: ( rng p = F & dom p = Seg n ) ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r)

take the Point of M ; :: thesis: ex r being Real st union F c= Ball ( the Point of M,r)

take 0 ; :: thesis: union F c= Ball ( the Point of M,0)

union F = {} by A19, A18, RELAT_1:42, ZFMISC_1:2;

hence union F c= Ball ( the Point of M,0) ; :: thesis: verum

end;let p be FinSequence; :: thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball (x,r) )

assume A19: ( rng p = F & dom p = Seg n ) ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r)

take the Point of M ; :: thesis: ex r being Real st union F c= Ball ( the Point of M,r)

take 0 ; :: thesis: union F c= Ball ( the Point of M,0)

union F = {} by A19, A18, RELAT_1:42, ZFMISC_1:2;

hence union F c= Ball ( the Point of M,0) ; :: thesis: verum

ex x being Point of M ex r being Real st union F c= Ball (x,r) ; :: thesis: verum

hence for F being Subset-Family of M st F is finite & F is being_ball-family holds

for n being Nat

for p being FinSequence st rng p = F & dom p = Seg n holds

ex x being Point of M ex r being Real st union F c= Ball (x,r) ; :: thesis: verum

hence ex x being Point of M ex r being Real st union F c= Ball (x,r) by A2, A4, A3; :: thesis: verum