let M be non empty MetrSpace; :: thesis: ( M is complete iff 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 )
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: ( ( 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 ) implies M is complete )

proof

reconsider NULL = 0 as Real ;
deffunc H₁( Element of NAT ) -> Element of REAL = 1 / (1 + $1);
assume A1: M is complete ; :: thesis: 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
consider seq being Real_Sequence such that
A2: for n being Element of NAT holds seq . n = H₁(n) from SEQ_1:sch 1();
set Ns = NULL (#) seq;
let F be Subset-Family of (TopSpaceMetr M); :: thesis: ( 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 ) ) implies not meet F is empty )
assume that
A3: F is closed and
A4: F is centered and
A5: 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: not meet F is empty
A6: for n being Element of NAT holds seq . n = 1 / (n + 1) by A2;
then A7: NULL (#) seq is convergent by SEQ_2:7, SEQ_4:30;
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) );
A8: 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: ( x in NAT implies ex y being set st
( y in bool the carrier of M & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in bool the carrier of M & S₁[x,y] )
then reconsider i = x as Element of NAT ;
consider A being Subset of M such that
A9: A in F and
A10: A is bounded and
A11: diameter A < 1 / (i + 1) by A5, XREAL_1:139;
take A ; :: thesis: ( A in bool the carrier of M & S₁[x,A] )
thus ( A in bool the carrier of M & S₁[x,A] ) by A9, A10, A11; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in F )
assume x in rng f ; :: thesis: x in F
then consider y being set such that
A13: y in dom f and
A14: f . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A13;
f . y in F by A12;
hence x in F by A14; :: thesis: verum

end;

then consider R being SetSequence of (TopSpaceMetr M) such that
A15: R is non-ascending and
A16: ( F is centered implies R is non-empty ) and
( F is open implies R is open ) and
A17: ( F is closed implies R is closed ) and
A18: for i being natural number holds R . i = meet { (f . j) where j is Element of NAT : j <= i } by Th13;
reconsider R9 = R as non-empty SetSequence of M by A4, A16;

now

let i be natural number ; :: thesis: R9 . i is bounded
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:3;
then R . i c= f . 0 by A18;
hence R9 . i is bounded by A12, TBSP_1:14; :: thesis: verum

end;

then reconsider R9 = R9 as non-empty bounded SetSequence of M by Def1;
set dR = diameter R9;

A19: now

let n be Element of NAT ; :: thesis: ( (NULL (#) seq) . n <= (diameter R9) . n & (diameter R9) . n <= seq . n )
set Sn = { (f . j) where j is Element of NAT : j <= n } ;
A20: 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 A18;
then A21: R . n c= f . n by A20, SETFAM_1:3;
then diameter (R9 . n) <= diameter (f . n) by A12, TBSP_1:24;
then A22: diameter (R9 . n) <= H₁(n) by A12, XXREAL_0:2;
f . n is bounded by A12;
then A23: 0 <= diameter (R9 . n) by A21, TBSP_1:14, TBSP_1:21;
A24: (NULL (#) seq) . n = NULL * (seq . n) by SEQ_1:9;
H₁(n) = seq . n by A2;
hence ( (NULL (#) seq) . n <= (diameter R9) . n & (diameter R9) . n <= seq . n ) by A23, A22, A24, Def2; :: thesis: verum

end;

A25: lim seq = 0 by A6, SEQ_4:30;
then A26: lim (NULL (#) seq) = NULL * 0 by A6, SEQ_2:8, SEQ_4:30;
A27: seq is convergent by A6, SEQ_4:30;
then A28: lim (diameter R9) = 0 by A25, A7, A26, A19, SEQ_2:20;
A29: R9 is closed by A3, A17, Th7;
then meet R9 <> {} by A1, A15, A28, Th10;
then consider x0 being set such that
A30: x0 in meet R9 by XBOOLE_0:def 1;
reconsider x0 = x0 as Point of M by A30;
A31: diameter R9 is convergent by A27, A25, A7, A26, A19, SEQ_2:19;

A32: now

let y be set ; :: thesis: ( y in F implies x0 in y )
assume A33: y in F ; :: thesis: x0 in y
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;
A34: 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: ( x in NAT implies ex z being set st
( z in bool the carrier of M & S₂[x,z] ) )
assume x in NAT ; :: thesis: ex z being set st
( z in bool the carrier of M & S₂[x,z] )
then reconsider i = x as Element of NAT ;
take (R . i) /\ Y ; :: thesis: ( (R . i) /\ Y in bool the carrier of M & S₂[x,(R . i) /\ Y] )
thus ( (R . i) /\ Y in bool the carrier of M & S₂[x,(R . i) /\ Y] ) ; :: thesis: verum

end;

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

A36: now

deffunc H₂( set ) -> set = f . $1;
let x be set ; :: thesis: ( x in dom f9 implies not f9 . x is empty )
assume x in dom f9 ; :: thesis: not f9 . x is empty
then reconsider i = x as Element of NAT ;
set SS = { (f . j) where j is Element of NAT : j <= i } ;
A37: f . i in { (f . j) where j is Element of NAT : j <= i } ;
A38: { (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: ( not x in { (f . j) where j is Element of NAT : j <= i } or x in { H₂(j) where j is Element of NAT : j in i + 1 } )
assume x in { (f . j) where j is Element of NAT : j <= i } ; :: thesis: x in { H₂(j) where j is Element of NAT : j in i + 1 }
then consider j being Element of NAT such that
A39: x = f . j and
A40: j <= i ;
j < i + 1 by A40, NAT_1:13;
then j in i + 1 by NAT_1:44;
hence x in { H₂(j) where j is Element of NAT : j in i + 1 } by A39; :: thesis: verum

end;

A41: {Y} \/ { (f . j) where j is Element of NAT : j <= i } c= F

proof

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

per cases ( z in {Y} or z in { (f . j) where j is Element of NAT : j <= i } ) by A42, XBOOLE_0:def 3;

suppose z in {Y} ; :: thesis: z in F

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

end;

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

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

end;

end;

end;

A43: i + 1 is finite ;
{ H₂(j) where j is Element of NAT : j in i + 1 } is finite from FRAENKEL:sch 21(A43);
then meet ({Y} \/ { (f . j) where j is Element of NAT : j <= i } ) <> {} by A4, A41, A38, FINSET_1:def 3;
then (meet {Y}) /\ (meet { (f . j) where j is Element of NAT : j <= i } ) <> {} by A37, SETFAM_1:9;
then Y /\ (meet { (f . j) where j is Element of NAT : j <= i } ) <> {} by SETFAM_1:10;
then Y /\ (R . i) <> {} by A18;
hence not f9 . x is empty by A35; :: thesis: verum

end;

A44: now

let i be natural number ; :: thesis: f9 . i is closed
reconsider Ri = R . i as Subset of (TopSpaceMetr M) ;
i in NAT by ORDINAL1:def 12;
then A45: f9 . i = Ri /\ Y by A35;
R9 . i is closed by A29, Def8;
then A46: Ri is closed by Th6;
Y is closed by A3, A33, TOPS_2:def 2;
hence f9 . i is closed by A46, A45, Th6; :: thesis: verum

end;

now

let i be natural number ; :: thesis: f9 . i is bounded
i in NAT by ORDINAL1:def 12;
then A47: f9 . i = (R9 . i) /\ Y by A35;
R9 . i is bounded by Def1;
hence f9 . i is bounded by A47, TBSP_1:14, XBOOLE_1:17; :: thesis: verum

end;

then reconsider f9 = f9 as non-empty bounded closed SetSequence of M by A36, A44, Def1, Def8, FUNCT_1:def 9;
A48: f9 . 0 = (R . 0) /\ Y by A35;
set df = diameter f9;

now

reconsider Y9 = Y as Subset of M ;
let n be Element of NAT ; :: thesis: ( (NULL (#) seq) . n <= (diameter f9) . n & (diameter f9) . n <= (diameter R9) . n )
A49: (NULL (#) seq) . n = NULL * (seq . n) by SEQ_1:9;
A50: (R . n) /\ Y9 = f9 . n by A35;
A51: R9 . n is bounded by Def1;
then diameter (f9 . n) <= diameter (R9 . n) by A50, TBSP_1:24, XBOOLE_1:17;
then A52: diameter (f9 . n) <= (diameter R9) . n by Def2;
(R . n) /\ Y c= R . n by XBOOLE_1:17;
then 0 <= diameter (f9 . n) by A51, A50, TBSP_1:14, TBSP_1:21;
hence ( (NULL (#) seq) . n <= (diameter f9) . n & (diameter f9) . n <= (diameter R9) . n ) by A52, A49, Def2; :: thesis: verum

end;

then A53: lim (diameter f9) = 0 by A7, A26, A31, A28, SEQ_2:20;

now

let i be Element of NAT ; :: thesis: f9 . (i + 1) c= f9 . i
A54: f9 . i = (R . i) /\ Y by A35;
A55: R . (i + 1) c= R . i by A15, KURATO_0:def 3;
f9 . (i + 1) = (R . (i + 1)) /\ Y by A35;
hence f9 . (i + 1) c= f9 . i by A54, A55, XBOOLE_1:26; :: thesis: verum

end;

then f9 is non-ascending by KURATO_0:def 3;
then meet f9 <> {} by A1, A53, Th10;
then consider z being set such that
A56: z in meet f9 by XBOOLE_0:def 1;
reconsider z = z as Point of M by A56;
A57: x0 = z

proof

assume x0 <> z ; :: thesis: contradiction
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
A58: for j being Element of NAT st i <= j holds
abs (((diameter R9) . j) - 0) < dist (x0,z) by A31, A28, SEQ_2:def 7;
A59: f9 . i = (R . i) /\ Y by A35;
z in f9 . i by A56, KURATO_0:3;
then A60: z in R . i by A59, XBOOLE_0:def 4;
A61: R9 . i is bounded by Def1;
then A62: 0 <= diameter (R9 . i) by TBSP_1:21;
x0 in R . i by A30, KURATO_0:3;
then dist (x0,z) <= diameter (R9 . i) by A60, A61, TBSP_1:def 8;
then A63: abs (diameter (R9 . i)) >= dist (x0,z) by A62, ABSVALUE:def 1;
abs (((diameter R9) . i) - 0) < dist (x0,z) by A58;
hence contradiction by A63, Def2; :: thesis: verum

end;

z in f9 . 0 by A56, KURATO_0:3;
hence x0 in y by A57, A48, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

assume A64: 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: M is complete

now

let S be non-empty bounded closed SetSequence of M; :: thesis: ( S is non-ascending & lim (diameter S) = 0 implies not meet S is empty )
assume that
A65: S is non-ascending and
A66: lim (diameter S) = 0 ; :: thesis: not meet S is empty
reconsider RS = rng S as Subset-Family of (TopSpaceMetr M) ;

A67: now

set d = diameter S;
A68: dom S = NAT by FUNCT_2:def 1;
A69: diameter S is bounded_below by Th1;
A70: diameter S is non-increasing by A65, Th2;
let r be Real; :: thesis: ( r > 0 implies ex Sn being Element of bool the carrier of M st
( Sn in RS & Sn is bounded & diameter Sn < r ) )
assume r > 0 ; :: thesis: ex Sn being Element of bool the carrier of M st
( Sn in RS & Sn is bounded & diameter Sn < r )
then consider n being Element of NAT such that
A71: for m being Element of NAT st n <= m holds
abs (((diameter S) . m) - 0) < r by A66, A69, A70, SEQ_2:def 7;
take Sn = S . n; :: thesis: ( Sn in RS & Sn is bounded & diameter Sn < r )
A72: (diameter S) . n = diameter Sn by Def2;
Sn is bounded by Def1;
then A73: diameter Sn >= 0 by TBSP_1:21;
abs (((diameter S) . n) - 0) < r by A71;
hence ( Sn in RS & Sn is bounded & diameter Sn < r ) by A72, A73, A68, Def1, ABSVALUE:def 1, FUNCT_1:def 3; :: thesis: verum

end;

RS is closed by Th12;
then not meet RS is empty by A64, A65, A67, Th11;
then consider x being set such that
A74: x in meet RS by XBOOLE_0:def 1;

now

let i be Element of NAT ; :: thesis: x in S . i
dom S = NAT by FUNCT_2:def 1;
then S . i in RS by FUNCT_1:def 3;
hence x in S . i by A74, SETFAM_1:def 1; :: thesis: verum

end;

hence not meet S is empty by KURATO_0:3; :: thesis: verum

end;

hence M is complete by Th10; :: thesis: verum