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₁( Nat) -> set = 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 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 Nat holds seq . n = 1 / (n + 1) by A2;
then A7: NULL (#) seq is convergent by SEQ_2:7, SEQ_4:31;
defpred S₁[ object , object ] means for i being Nat 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 object st x in NAT holds
ex y being object st
( y in bool the carrier of M & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in bool the carrier of M & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in bool the carrier of M & S₁[x,y] )
then reconsider i = x as 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 object st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A8);
rng f c= F

proof

let x be object ; :: 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 object 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 Nat 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 :: thesis: for i being Nat holds R9 . i is bounded

let i be Nat; :: 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 pointwise_bounded SetSequence of M by Def1;
set dR = diameter R9;

A19: now :: thesis: for n being Nat holds
( (NULL (#) seq) . n <= (diameter R9) . n & (diameter R9) . n <= seq . n )

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

end;

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

A33: now :: thesis: for y being set st y in F holds
x0 in y

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

proof

let x be object ; :: thesis: ( x in NAT implies ex z being object st
( z in bool the carrier of M & S₂[x,z] ) )
assume x in NAT ; :: thesis: ex z being object st
( z in bool the carrier of M & S₂[x,z] )
then reconsider i = x as 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
A36: for x being object st x in NAT holds
S₂[x,f9 . x] from FUNCT_2:sch 1(A35);

A37: now :: thesis: for x being object st x in dom f9 holds
not f9 . x is empty

deffunc H₂( object ) -> set = f . $1;
let x be object ; :: 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 } ;
A38: f . i in { (f . j) where j is Element of NAT : j <= i } ;
A39: { (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 object ; :: 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
A40: x = f . j and
A41: j <= i ;
j < i + 1 by A41, NAT_1:13;
then j in Segm (i + 1) by NAT_1:44;
hence x in { H₂(j) where j is Element of NAT : j in i + 1 } by A40; :: thesis: verum

end;

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

proof

let z be object ; :: 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 A43: 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 A43, XBOOLE_0:def 3;

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

hence z in F by A34, 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;

A44: i + 1 is finite ;
{ H₂(j) where j is Element of NAT : j in i + 1 } is finite from FRAENKEL:sch 21(A44);
then meet ({Y} \/ { (f . j) where j is Element of NAT : j <= i } ) <> {} by A4, A42, A39, FINSET_1:def 3;
then (meet {Y}) /\ (meet { (f . j) where j is Element of NAT : j <= i } ) <> {} by A38, 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 A36; :: thesis: verum

end;

A45: now :: thesis: for i being Nat holds f9 . i is closed

let i be Nat; :: thesis: f9 . i is closed
reconsider Ri = R . i as Subset of (TopSpaceMetr M) ;
i in NAT by ORDINAL1:def 12;
then A46: f9 . i = Ri /\ Y by A36;
R9 . i is closed by A30;
then A47: Ri is closed by Th6;
Y is closed by A3, A34;
hence f9 . i is closed by A47, A46, Th6; :: thesis: verum

end;

now :: thesis: for i being Nat holds f9 . i is bounded

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

end;

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

now :: thesis: for n being Nat holds
( (NULL (#) seq) . n <= (diameter f9) . n & (diameter f9) . n <= (diameter R9) . n )

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

end;

then A54: lim (diameter f9) = 0 by A7, A27, A32, A29, SEQ_2:20;

now :: thesis: for i being Nat holds f9 . (i + 1) c= f9 . i

let i be Nat; :: thesis: f9 . (i + 1) c= f9 . i
i in NAT by ORDINAL1:def 12;
then A55: f9 . i = (R . i) /\ Y by A36;
A56: R . (i + 1) c= R . i by A15, KURATO_0:def 3;
f9 . (i + 1) = (R . (i + 1)) /\ Y by A36;
hence f9 . (i + 1) c= f9 . i by A55, A56, XBOOLE_1:26; :: thesis: verum

end;

then f9 is non-ascending by KURATO_0:def 3;
then meet f9 <> {} by A1, A54, Th10;
then consider z being object such that
A57: z in meet f9 by XBOOLE_0:def 1;
reconsider z = z as Point of M by A57;
A58: 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 Nat such that
A59: for j being Nat st i <= j holds
|.(((diameter R9) . j) - 0).| < dist (x0,z) by A32, A29, SEQ_2:def 7;
A60: i in NAT by ORDINAL1:def 12;
A61: f9 . i = (R . i) /\ Y by A36, A60;
z in f9 . i by A57, KURATO_0:3;
then A62: z in R . i by A61, XBOOLE_0:def 4;
A63: R9 . i is bounded by Def1;
then A64: 0 <= diameter (R9 . i) by TBSP_1:21;
x0 in R . i by A31, KURATO_0:3;
then dist (x0,z) <= diameter (R9 . i) by A62, A63, TBSP_1:def 8;
then A65: |.(diameter (R9 . i)).| >= dist (x0,z) by A64, ABSVALUE:def 1;
|.(((diameter R9) . i) - 0).| < dist (x0,z) by A59;
hence contradiction by A65, Def2; :: thesis: verum

end;

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

end;

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

end;

assume A66: 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 :: thesis: for S being non-empty pointwise_bounded closed SetSequence of M st S is non-ascending & lim (diameter S) = 0 holds
not meet S is empty

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

A69: now :: thesis: for r being Real st r > 0 holds
ex Sn being Element of bool the carrier of M st
( Sn in RS & Sn is bounded & diameter Sn < r )

set d = diameter S;
A70: dom S = NAT by FUNCT_2:def 1;
A71: diameter S is bounded_below by Th1;
A72: diameter S is non-increasing by A67, 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 Nat such that
A73: for m being Nat st n <= m holds
|.(((diameter S) . m) - 0).| < r by A68, A71, A72, SEQ_2:def 7;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
take Sn = S . nn; :: thesis: ( Sn in RS & Sn is bounded & diameter Sn < r )
A74: (diameter S) . n = diameter Sn by Def2;
Sn is bounded by Def1;
then A75: diameter Sn >= 0 by TBSP_1:21;
|.(((diameter S) . n) - 0).| < r by A73;
hence ( Sn in RS & Sn is bounded & diameter Sn < r ) by A74, A75, A70, Def1, ABSVALUE:def 1, FUNCT_1:def 3; :: thesis: verum

end;

RS is closed by Th12;
then not meet RS is empty by A66, A67, A69, Th11;
then consider x being object such that
A76: x in meet RS by XBOOLE_0:def 1;

now :: thesis: for i being Nat holds x in S . i

let i be Nat; :: thesis: x in S . i
A77: i in NAT by ORDINAL1:def 12;
dom S = NAT by FUNCT_2:def 1;
then S . i in RS by FUNCT_1:def 3, A77;
hence x in S . i by A76, 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