let M be non empty MetrSpace; :: thesis: ( M is complete iff for S being non-empty bounded closed SetSequence of M st S is non-ascending & lim (diameter S) = 0 holds
not meet S is empty )
set T = TopSpaceMetr M;
thus ( M is complete implies for S being non-empty bounded closed SetSequence of M st S is non-ascending & lim (diameter S) = 0 holds
not meet S is empty ) :: thesis: ( ( for S being non-empty bounded closed SetSequence of M st S is non-ascending & lim (diameter S) = 0 holds
not meet S is empty ) implies M is complete )

proof

assume A1: M is complete ; :: thesis: for S being non-empty 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 bounded closed SetSequence of M; :: thesis: ( S is non-ascending & lim (diameter S) = 0 implies not meet S is empty )
assume A2: ( S is non-ascending & lim (diameter S) = 0 ) ; :: thesis: not meet S is empty
defpred S₁[ set , set ] means $2 in S . $1;
A3: for x being set st x in NAT holds
ex y being set st
( y in the carrier of M & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in the carrier of M & S₁[x,y] ) )
assume A4: x in NAT ; :: thesis: ex y being set st
( y in the carrier of M & S₁[x,y] )
A5: dom S = NAT by FUNCT_2:def 1;
then not S . x is empty by A4, FUNCT_1:def 15;
then consider y being set such that
A6: y in S . x by XBOOLE_0:def 1;
( S . x in rng S & rng S c= bool the carrier of M ) by A4, A5, FUNCT_1:def 5;
hence ex y being set st
( y in the carrier of M & S₁[x,y] ) by A6; :: thesis: verum

end;

consider F being Function of NAT ,the carrier of M such that
A7: for x being set st x in NAT holds
S₁[x,F . x] from FUNCT_2:sch 1(A3);

now

let i be natural number ; :: thesis: F . i in S . i
i in NAT by ORDINAL1:def 13;
hence F . i in S . i by A7; :: thesis: verum

end;

then F is Cauchy by A2, Th4;
then F is convergent by A1, TBSP_1:def 6;
then consider x being Point of M such that
A8: F is_convergent_in_metrspace_to x by METRIC_6:22;
reconsider x' = x as Point of (TopSpaceMetr M) ;
reconsider F' = F as sequence of (TopSpaceMetr M) ;

now

let i be Element of NAT ; :: thesis: x in S . i
set F1 = F' ^\ i;
reconsider Si = S . i as Subset of (TopSpaceMetr M) ;
S . i is closed by Def8;
then A10: Si is closed by Th6;
rng (F' ^\ i) c= Si

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (F' ^\ i) or x in Si )
assume A11: x in rng (F' ^\ i) ; :: thesis: x in Si
consider y being set such that
A12: ( y in dom (F' ^\ i) & (F' ^\ i) . y = x ) by A11, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A12;
( x = F . (y + i) & i <= y + i ) by NAT_1:def 3, A12, NAT_1:11;
then ( x in S . (y + i) & S . (y + i) c= S . i ) by A2, A7, PROB_1:def 6;
hence x in Si ; :: thesis: verum

end;

then A13: Lim (F' ^\ i) c= Si by A10, FRECHET2:12;
F' is_convergent_to x' by A8, FRECHET2:31;
then F' ^\ i is_convergent_to x' by FRECHET2:18;
then x in Lim (F' ^\ i) by FRECHET:def 4;
hence x in S . i by A13; :: thesis: verum

end;

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

end;

assume A14: for S being non-empty bounded closed SetSequence of M st S is non-ascending & lim (diameter S) = 0 holds
not meet S is empty ; :: thesis: M is complete
let F be sequence of M; :: according to TBSP_1:def 6 :: thesis: ( not F is Cauchy or F is convergent )
assume A15: F is Cauchy ; :: thesis: F is convergent
consider S being non-empty closed SetSequence of M such that
A16: S is non-ascending and
A17: ( F is Cauchy implies ( S is bounded & lim (diameter S) = 0 ) ) and
A18: for i being natural number ex U being Subset of (TopSpaceMetr M) st
( U = { (F . j) where j is Element of NAT : j >= i } & S . i = Cl U ) by Th9;
not meet S is empty by A14, A15, A16, A17;
then consider x being set such that
A19: x in meet S by XBOOLE_0:def 1;
reconsider x = x as Point of M by A19;
take x ; :: according to TBSP_1:def 3 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= dist (F . b₃),x ) )
let r be Real; :: thesis: ( r <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not r <= dist (F . b₂),x ) )
assume A20: r > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not r <= dist (F . b₂),x )
set d = diameter S;
( diameter S is bounded_below & diameter S is non-increasing ) by A15, A16, A17, Th1, Th2;
then consider n being Element of NAT such that
A21: for m being Element of NAT st n <= m holds
abs (((diameter S) . m) - 0 ) < r by A15, A17, A20, SEQ_2:def 7;
take n ; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not r <= dist (F . b₁),x )
let m be Element of NAT ; :: thesis: ( not n <= m or not r <= dist (F . m),x )
assume A22: n <= m ; :: thesis: not r <= dist (F . m),x
consider U being Subset of (TopSpaceMetr M) such that
A23: ( U = { (F . j) where j is Element of NAT : j >= m } & S . m = Cl U ) by A18;
( F . m in U & U c= Cl U ) by A23, PRE_TOPC:48;
then ( x in S . m & F . m in S . m & S . m is bounded ) by A15, A17, A19, A23, Def1, KURATO_2:6;
then ( dist (F . m),x <= diameter (S . m) & diameter (S . m) >= 0 & diameter (S . m) = (diameter S) . m & abs (((diameter S) . m) - 0 ) < r ) by A21, A22, Def2, TBSP_1:29, TBSP_1:def 10;
then ( dist (F . m),x <= (diameter S) . m & (diameter S) . m < r ) by ABSVALUE:def 1;
hence not r <= dist (F . m),x by XXREAL_0:2; :: thesis: verum