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

proof

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

end;

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

now

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

end;

then F is Cauchy by A2, A3, Th4;
then F is convergent by A1, TBSP_1:def 5;
then consider x being Point of M such that
A9: F is_convergent_in_metrspace_to x by METRIC_6:10;
reconsider F9 = F as sequence of (TopSpaceMetr M) ;
reconsider x9 = x as Point of (TopSpaceMetr M) ;

now

let i be Element of NAT ; :: thesis: x in S . i
set F1 = F9 ^\ i;
reconsider Si = S . i as Subset of (TopSpaceMetr M) ;
A10: rng (F9 ^\ i) c= Si

proof

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

end;

F9 is_convergent_to x9 by A9, FRECHET2:28;
then F9 ^\ i is_convergent_to x9 by FRECHET2:15;
then A14: x in Lim (F9 ^\ i) by FRECHET:def 5;
S . i is closed by Def8;
then Si is closed by Th6;
then Lim (F9 ^\ i) c= Si by A10, FRECHET2:9;
hence x in S . i by A14; :: thesis: verum

end;

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

end;

assume A15: 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 5 :: thesis: ( not F is Cauchy or F is convergent )
assume A16: F is Cauchy ; :: thesis: F is convergent
consider S being non-empty closed SetSequence of M such that
A17: S is non-ascending and
A18: ( F is Cauchy implies ( S is bounded & lim (diameter S) = 0 ) ) and
A19: 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;
set d = diameter S;
A20: diameter S is non-increasing by A16, A17, A18, Th2;
not meet S is empty by A15, A16, A17, A18;
then consider x being set such that
A21: x in meet S by XBOOLE_0:def 1;
A22: diameter S is bounded_below by A16, A18, Th1;
reconsider x = x as Point of M by A21;
take x ; :: according to TBSP_1:def 2 :: 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 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) )
then consider n being Element of NAT such that
A23: for m being Element of NAT st n <= m holds
abs (((diameter S) . m) - 0) < r by A16, A18, A22, 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 n <= m ; :: thesis: not r <= dist ((F . m),x)
then A24: abs (((diameter S) . m) - 0) < r by A23;
A25: S . m is bounded by A16, A18, Def1;
A26: x in S . m by A21, KURATO_0:3;
A27: diameter (S . m) = (diameter S) . m by Def2;
consider U being Subset of (TopSpaceMetr M) such that
A28: U = { (F . j) where j is Element of NAT : j >= m } and
A29: S . m = Cl U by A19;
A30: U c= Cl U by PRE_TOPC:18;
F . m in U by A28;
then A31: dist ((F . m),x) <= diameter (S . m) by A29, A30, A26, A25, TBSP_1:def 8;
diameter (S . m) >= 0 by A25, TBSP_1:21;
then (diameter S) . m < r by A27, A24, ABSVALUE:def 1;
hence not r <= dist ((F . m),x) by A31, A27, XXREAL_0:2; :: thesis: verum