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

proof

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

proof

A5: dom S = NAT by FUNCT_2:def 1;
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in the carrier of M & S₁[x,y] ) )
assume A6: x in NAT ; :: thesis: ex y being object 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 object 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 object st
( y in the carrier of M & S₁[x,y] ) by A7; :: thesis: verum

end;

consider F being sequence of the carrier of M such that
A8: for x being object st x in NAT holds
S₁[x,F . x] from FUNCT_2:sch 1(A4);
for i being Nat holds F . i in S . i by A8, ORDINAL1:def 12;
then F is Cauchy by A2, A3, Th4;
then F is convergent by A1;
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 :: thesis: for i being Nat holds x in S . i

let i be 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 object ; :: 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 object 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;
A14: y + i in NAT by ORDINAL1:def 12;
x = F . (y + i) by A12, NAT_1:def 3;
then x in S . (y + i) by A8, A14;
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 A15: 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 A15; :: thesis: verum

end;

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

end;

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