let M be non empty MetrSpace; :: thesis:
set T = TopSpaceMetr M;
thus ( M is complete implies for F being Subset-Family of (TopSpaceMetr M) st F is closed & F is centered & ( for r being Real st r > 0 holds
ex A being Subset of M st
( A in F & A is bounded & diameter A < r ) ) holds
not meet F is empty ) :: thesis:

proof

assume A1: M is complete ; :: thesis:
let F be Subset-Family of (TopSpaceMetr M); :: thesis:
assume that
A2: ( F is closed & F is centered ) and
A3: for r being Real st r > 0 holds
ex A being Subset of M st
( A in F & A is bounded & diameter A < r ) ; :: thesis:
defpred S₁[ set , set ] means for i being natural number st i = $1 holds
for A being Subset of M st A = $2 holds
( A in F & A is bounded & diameter A < 1 / (i + 1) );
A4: for x being set st x in NAT holds
ex y being set st
( y in bool the carrier of M & S₁[x,y] )

proof

let x be set ; :: thesis:
assume A5: x in NAT ; :: thesis:
reconsider i = x as Element of NAT by A5;
consider A being Subset of M such that
A6: ( A in F & A is bounded & diameter A < 1 / (i + 1) ) by A3, XREAL_1:141;
take A ; :: thesis:
thus ( A in bool the carrier of M & S₁[x,A] ) by A6; :: thesis:

end;

consider f being SetSequence of M such that
A7: for x being set st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A4);
rng f c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in rng f ; :: thesis:
consider y being set such that
A9: ( y in dom f & f . y = x ) by A8, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A9;
f . y in F by A7;
hence x in F by A9; :: thesis:

end;

then consider R being SetSequence of (TopSpaceMetr M) such that
A10: R is non-ascending and
A11: ( F is centered implies R is non-empty ) and
( F is open implies R is open ) and
A12: ( F is closed implies R is closed ) and
A13: for i being natural number holds R . i = meet { (f . j) where j is Element of NAT : j <= i } by Th13;
reconsider R' = R as non-empty SetSequence of M by A2, A11;

now

let i be natural number ; :: thesis:
f . 0 in { (f . j) where j is Element of NAT : j <= i } ;
then meet { (f . j) where j is Element of NAT : j <= i } c= f . 0 by SETFAM_1:4;
then ( R . i c= f . 0 & f . 0 is bounded ) by A7, A13;
hence R' . i is bounded by TBSP_1:21; :: thesis:

end;

then reconsider R' = R' as non-empty bounded SetSequence of M by Def1;
A14: ( R' is closed & R' is non-ascending ) by A2, A10, A12, Th7;
deffunc H₁( Element of NAT ) -> Element of REAL = 1 / (1 + $1);
consider seq being Real_Sequence such that
A15: for n being Element of NAT holds seq . n = H₁(n) from SEQ_1:sch 1();
reconsider NULL = 0 as Real ;
set Ns = NULL (#) seq;
for n being Element of NAT holds seq . n = 1 / (n + 1) by A15;
then A16: ( seq is convergent & lim seq = 0 ) by SEQ_4:45;
then A17: ( NULL (#) seq is convergent & lim (NULL (#) seq) = NULL * 0 ) by SEQ_2:21, SEQ_2:22;
set dR = diameter R';

now

let n be Element of NAT ; :: thesis:
set Sn = { (f . j) where j is Element of NAT : j <= n } ;
( f . n in { (f . j) where j is Element of NAT : j <= n } & R . n = meet { (f . j) where j is Element of NAT : j <= n } ) by A13;
then ( R . n c= f . n & f . n is bounded ) by A7, SETFAM_1:4;
then ( diameter (R' . n) <= diameter (f . n) & diameter (f . n) < H₁(n) & R' . n is bounded ) by A7, TBSP_1:21, TBSP_1:32;
then ( 0 <= diameter (R' . n) & diameter (R' . n) <= H₁(n) & (NULL (#) seq) . n = NULL * (seq . n) & H₁(n) = seq . n & diameter (R' . n) = (diameter R') . n ) by A15, Def2, SEQ_1:13, TBSP_1:29, XXREAL_0:2;
hence ( (NULL (#) seq) . n <= (diameter R') . n & (diameter R') . n <= seq . n ) ; :: thesis:

end;

then A18: ( diameter R' is convergent & lim (diameter R') = 0 ) by A16, A17, SEQ_2:33, SEQ_2:34;
then meet R' <> {} by A1, A14, Th10;
then consider x0 being set such that
A19: x0 in meet R' by XBOOLE_0:def 1;
reconsider x0 = x0 as Point of M by A19;

A20: now

let y be set ; :: thesis:
assume A21: y in F ; :: thesis:
then reconsider Y = y as Subset of (TopSpaceMetr M) ;
defpred S₂[ set , set ] means for i being natural number st i = $1 holds
$2 = (R . i) /\ Y;
A22: for x being set st x in NAT holds
ex z being set st
( z in bool the carrier of M & S₂[x,z] )

proof

let x be set ; :: thesis:
assume A23: x in NAT ; :: thesis:
reconsider i = x as Element of NAT by A23;
take (R . i) /\ Y ; :: thesis:
thus ( (R . i) /\ Y in bool the carrier of M & S₂[x,(R . i) /\ Y] ) ; :: thesis:

end;

consider f' being SetSequence of M such that
A24: for x being set st x in NAT holds
S₂[x,f' . x] from FUNCT_2:sch 1(A22);

A25: now

let x be set ; :: thesis:
assume A26: x in dom f' ; :: thesis:
reconsider i = x as Element of NAT by A26;
set SS = { (f . j) where j is Element of NAT : j <= i } ;
A27: ( Y in {Y} & f . i in { (f . j) where j is Element of NAT : j <= i } ) by TARSKI:def 1;
A28: {Y} \/ { (f . j) where j is Element of NAT : j <= i } c= F

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A29: z in {Y} \/ { (f . j) where j is Element of NAT : j <= i } ; :: thesis:

per cases by A29, XBOOLE_0:def 3;

suppose z in {Y} ; :: thesis:

hence z in F by A21, TARSKI:def 1; :: thesis:

end;

suppose z in { (f . j) where j is Element of NAT : j <= i } ; :: thesis:

then ex j being Element of NAT st
( z = f . j & j <= i ) ;
hence z in F by A7; :: thesis:

end;

A30: i + 1 is finite ;
deffunc H₂( set ) -> set = f . $1;
A31: { H₂(j) where j is Element of NAT : j in i + 1 } is finite from FRAENKEL:sch 21(A30);
{ (f . j) where j is Element of NAT : j <= i } c= { H₂(j) where j is Element of NAT : j in i + 1 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A32: x in { (f . j) where j is Element of NAT : j <= i } ; :: thesis:
consider j being Element of NAT such that
A33: ( x = f . j & j <= i ) by A32;
j < i + 1 by A33, NAT_1:13;
then j in i + 1 by NAT_1:45;
hence x in { H₂(j) where j is Element of NAT : j in i + 1 } by A33; :: thesis:

end;

then meet ({Y} \/ { (f . j) where j is Element of NAT : j <= i } ) <> {} by A2, A28, FINSET_1:def 3, A31;
then (meet {Y}) /\ (meet { (f . j) where j is Element of NAT : j <= i } ) <> {} by A27, SETFAM_1:10;
then Y /\ (meet { (f . j) where j is Element of NAT : j <= i } ) <> {} by SETFAM_1:11;
then Y /\ (R . i) <> {} by A13;
hence not f' . x is empty by A24; :: thesis:

end;

A34: now

let i be natural number ; :: thesis:
i in NAT by ORDINAL1:def 13;
then ( f' . i = (R' . i) /\ Y & R' . i is bounded & (R . i) /\ Y c= R . i ) by A24, Def1, XBOOLE_1:17;
hence f' . i is bounded by TBSP_1:21; :: thesis:

end;

now

let i be natural number ; :: thesis:
reconsider Ri = R . i as Subset of (TopSpaceMetr M) ;
R' . i is closed by A14, Def8;
then ( Ri is closed & Y is closed & i in NAT ) by A2, A21, Th6, ORDINAL1:def 13, TOPS_2:def 2;
then ( Ri /\ Y is closed & f' . i = Ri /\ Y ) by A24, TOPS_1:35;
hence f' . i is closed by Th6; :: thesis:

end;

then reconsider f' = f' as non-empty bounded closed SetSequence of M by A25, A34, Def1, Def8, FUNCT_1:def 15;

now

let i be Element of NAT ; :: thesis:
( f' . (i + 1) = (R . (i + 1)) /\ Y & f' . i = (R . i) /\ Y & R . (i + 1) c= R . i ) by A10, A24, KURATO_2:def 5;
hence f' . (i + 1) c= f' . i by XBOOLE_1:26; :: thesis:

end;

then A35: f' is non-ascending by KURATO_2:def 5;
set df = diameter f';

now

let n be Element of NAT ; :: thesis:
reconsider Y' = Y as Subset of M ;
( R' . n is bounded & (R . n) /\ Y c= R . n & (R . n) /\ Y' = f' . n ) by A24, Def1, XBOOLE_1:17;
then ( f' . n is bounded & diameter (f' . n) <= diameter (R' . n) ) by TBSP_1:21, TBSP_1:32;
then ( 0 <= diameter (f' . n) & diameter (f' . n) <= (diameter R') . n & (NULL (#) seq) . n = NULL * (seq . n) ) by Def2, SEQ_1:13, TBSP_1:29;
hence ( (NULL (#) seq) . n <= (diameter f') . n & (diameter f') . n <= (diameter R') . n ) by Def2; :: thesis:

end;

then lim (diameter f') = 0 by A17, A18, SEQ_2:34;
then meet f' <> {} by A1, A35, Th10;
then consider z being set such that
A36: z in meet f' by XBOOLE_0:def 1;
reconsider z = z as Point of M by A36;
A37: x0 = z

proof

assume x0 <> z ; :: thesis:
then dist x0,z <> 0 by METRIC_1:2;
then dist x0,z > 0 by METRIC_1:5;
then consider i being Element of NAT such that
A38: for j being Element of NAT st i <= j holds
abs (((diameter R') . j) - 0 ) < dist x0,z by A18, SEQ_2:def 7;
( z in f' . i & f' . i = (R . i) /\ Y ) by A24, A36, KURATO_2:6;
then ( z in R . i & x0 in R . i & R' . i is bounded ) by A19, Def1, KURATO_2:6, XBOOLE_0:def 4;
then ( dist x0,z <= diameter (R' . i) & 0 <= diameter (R' . i) ) by TBSP_1:29, TBSP_1:def 10;
then ( abs (diameter (R' . i)) >= dist x0,z & abs (((diameter R') . i) - 0 ) < dist x0,z ) by A38, ABSVALUE:def 1;
hence contradiction by Def2; :: thesis:

end;

( z in f' . 0 & f' . 0 = (R . 0 ) /\ Y ) by A24, A36, KURATO_2:6;
hence x0 in y by A37, XBOOLE_0:def 4; :: thesis:

end;

F <> {} by A2, FINSET_1:def 3;
hence not meet F is empty by A20, SETFAM_1:def 1; :: thesis:

end;

assume A39: for F being Subset-Family of (TopSpaceMetr M) st F is closed & F is centered & ( for r being Real st r > 0 holds
ex A being Subset of M st
( A in F & A is bounded & diameter A < r ) ) holds
not meet F is empty ; :: thesis:

now

let S be non-empty bounded closed SetSequence of M; :: thesis:
assume A40: ( S is non-ascending & lim (diameter S) = 0 ) ; :: thesis:
reconsider RS = rng S as Subset-Family of (TopSpaceMetr M) ;
A41: ( RS is closed & RS is centered ) by A40, Th11, Th12;

now

let r be Real; :: thesis:
assume A42: r > 0 ; :: thesis:
set d = diameter S;
( diameter S is bounded_below & diameter S is non-increasing ) by A40, Th1, Th2;
then consider n being Element of NAT such that
A43: for m being Element of NAT st n <= m holds
abs (((diameter S) . m) - 0 ) < r by A40, A42, SEQ_2:def 7;
take Sn = S . n; :: thesis:
Sn is bounded by Def1;
then ( abs (((diameter S) . n) - 0 ) < r & (diameter S) . n = diameter Sn & diameter Sn >= 0 & dom S = NAT ) by A43, Def2, FUNCT_2:def 1, TBSP_1:29;
hence ( Sn in RS & Sn is bounded & diameter Sn < r ) by Def1, ABSVALUE:def 1, FUNCT_1:def 5; :: thesis:

end;

then not meet RS is empty by A39, A41;
then consider x being set such that
A44: x in meet RS by XBOOLE_0:def 1;

now

let i be Element of NAT ; :: thesis:
dom S = NAT by FUNCT_2:def 1;
then ( RS <> {} & S . i in RS ) by FUNCT_1:def 5, RELAT_1:65;
hence x in S . i by A44, SETFAM_1:def 1; :: thesis:

end;

hence not meet S is empty by KURATO_2:6; :: thesis:

end;

hence M is complete by Th10; :: thesis: