let M be non empty MetrSpace; :: thesis: ( M is complete implies for A being non empty Subset of M
for A9 being Subset of (TopSpaceMetr M) st A = A9 holds
( M | A is complete iff A9 is closed ) )
assume A1: M is complete ; :: thesis: for A being non empty Subset of M
for A9 being Subset of (TopSpaceMetr M) st A = A9 holds
( M | A is complete iff A9 is closed )
set T = TopSpaceMetr M;
let A be non empty Subset of M; :: thesis: for A9 being Subset of (TopSpaceMetr M) st A = A9 holds
( M | A is complete iff A9 is closed )
let A9 be Subset of (TopSpaceMetr M); :: thesis: ( A = A9 implies ( M | A is complete iff A9 is closed ) )
assume A2: A = A9 ; :: thesis: ( M | A is complete iff A9 is closed )
set MA = M | A;
set TA = TopSpaceMetr (M | A);
thus ( M | A is complete implies A9 is closed ) :: thesis: ( A9 is closed implies M | A is complete )

proof

assume A3: M | A is complete ; :: thesis: A9 is closed
A4: Cl A9 c= A9

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in Cl A9 or p in A9 )
assume A5: p in Cl A9 ; :: thesis: p in A9
reconsider p = p as Point of M by A5;
defpred S₁[ object , object ] means for i being Nat st i = $1 holds
$2 = A /\ (cl_Ball (p,(1 / (i + 1))));
A6: for x being object st x in NAT holds
ex y being object st
( y in bool the carrier of (M | A) & 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 | A) & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in bool the carrier of (M | A) & S₁[x,y] )
then reconsider i = x as Nat ;
take A /\ (cl_Ball (p,(1 / (i + 1)))) ; :: thesis: ( A /\ (cl_Ball (p,(1 / (i + 1)))) in bool the carrier of (M | A) & S₁[x,A /\ (cl_Ball (p,(1 / (i + 1))))] )
A /\ (cl_Ball (p,(1 / (i + 1)))) c= A by XBOOLE_1:17;
then A /\ (cl_Ball (p,(1 / (i + 1)))) c= the carrier of (M | A) by TOPMETR:def 2;
hence ( A /\ (cl_Ball (p,(1 / (i + 1)))) in bool the carrier of (M | A) & S₁[x,A /\ (cl_Ball (p,(1 / (i + 1))))] ) ; :: thesis: verum

end;

consider f being SetSequence of (M | A) such that
A7: for x being object st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A6);

A8: now :: thesis: for x being object st x in dom f holds
not f . x is empty

let x be object ; :: thesis: ( x in dom f implies not f . x is empty )
assume x in dom f ; :: thesis: not f . x is empty
then reconsider i = x as Element of NAT ;
reconsider B = Ball (p,(1 / (i + 1))) as Subset of (TopSpaceMetr M) ;
Ball (p,(1 / (i + 1))) in Family_open_set M by PCOMPS_1:29;
then A9: B is open by PRE_TOPC:def 2;
p in B by TBSP_1:11, XREAL_1:139;
then B meets A9 by A5, A9, PRE_TOPC:24;
then consider y being object such that
A10: y in B and
A11: y in A9 by XBOOLE_0:3;
reconsider y = y as Point of M by A10;
dist (p,y) < 1 / (i + 1) by A10, METRIC_1:11;
then y in cl_Ball (p,(1 / (i + 1))) by METRIC_1:12;
then y in A /\ (cl_Ball (p,(1 / (i + 1)))) by A2, A11, XBOOLE_0:def 4;
hence not f . x is empty by A7; :: thesis: verum

end;

A12: now :: thesis: for i being Nat holds f . i is closed

let i be Nat; :: thesis: f . i is closed
reconsider cB = cl_Ball (p,(1 / (i + 1))) as Subset of (TopSpaceMetr M) ;
reconsider fi = f . i as Subset of (TopSpaceMetr (M | A)) ;
A13: i in NAT by ORDINAL1:def 12;
([#] M) \ cB in Family_open_set M by NAGATA_1:14;
then cB ` is open by PRE_TOPC:def 2;
then A14: cB is closed by TOPS_1:3;
A15: TopSpaceMetr (M | A) = (TopSpaceMetr M) | A9 by A2, HAUSDORF:16;
then [#] ((TopSpaceMetr M) | A9) = A by TOPMETR:def 2;
then fi = cB /\ ([#] ((TopSpaceMetr M) | A9)) by A7, A13;
then fi is closed by A14, A15, PRE_TOPC:13;
hence f . i is closed by Th6; :: thesis: verum

end;

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

let i be Nat; :: thesis: f . i is bounded
set ACL = A /\ (cl_Ball (p,(1 / (i + 1))));
cl_Ball (p,(1 / (i + 1))) is bounded by TOPREAL6:59;
then A16: A /\ (cl_Ball (p,(1 / (i + 1)))) is bounded by TBSP_1:14, XBOOLE_1:17;
i in NAT by ORDINAL1:def 12;
then f . i = A /\ (cl_Ball (p,(1 / (i + 1)))) by A7;
hence f . i is bounded by A16, Th15; :: thesis: verum

end;

then reconsider f = f as non-empty pointwise_bounded closed SetSequence of (M | A) by A8, A12, Def1, Def8, FUNCT_1:def 9;
set df = diameter f;
reconsider NULL = 0 , TWO = 2 as Real ;
deffunc H₁( Nat) -> set = 1 / (1 + $1);
consider seq being Real_Sequence such that
A17: for n being Nat holds seq . n = H₁(n) from SEQ_1:sch 1();

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

let i be Nat; :: thesis: f . (i + 1) c= f . i
set i1 = i + 1;
cl_Ball (p,(1 / ((i + 1) + 1))) c= cl_Ball (p,(1 / (i + 1)))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cl_Ball (p,(1 / ((i + 1) + 1))) or x in cl_Ball (p,(1 / (i + 1))) )
assume A18: x in cl_Ball (p,(1 / ((i + 1) + 1))) ; :: thesis: x in cl_Ball (p,(1 / (i + 1)))
reconsider q = x as Point of M by A18;
i + 1 < (i + 1) + 1 by NAT_1:13;
then A19: 1 / ((i + 1) + 1) < 1 / (i + 1) by XREAL_1:76;
dist (p,q) <= 1 / ((i + 1) + 1) by A18, METRIC_1:12;
then dist (p,q) <= 1 / (i + 1) by A19, XXREAL_0:2;
hence x in cl_Ball (p,(1 / (i + 1))) by METRIC_1:12; :: thesis: verum

end;

then A20: A /\ (cl_Ball (p,(1 / ((i + 1) + 1)))) c= A /\ (cl_Ball (p,(1 / (i + 1)))) by XBOOLE_1:26;
i in NAT by ORDINAL1:def 12;
then f . i = A /\ (cl_Ball (p,(1 / (i + 1)))) by A7;
hence f . (i + 1) c= f . i by A7, A20; :: thesis: verum

end;

then A21: f is non-ascending by KURATO_0:def 3;
set Ts = TWO (#) seq;
set Ns = NULL (#) seq;
A22: for n being Nat holds seq . n = 1 / (n + 1) by A17;
then A23: NULL (#) seq is convergent by SEQ_2:7, SEQ_4:31;

A24: now :: thesis: for n being Nat holds
( (NULL (#) seq) . n <= (diameter f) . n & (diameter f) . n <= (TWO (#) seq) . n )

let n be Nat; :: thesis: ( (NULL (#) seq) . n <= (diameter f) . n & (diameter f) . n <= (TWO (#) seq) . n )
set cB = cl_Ball (p,(1 / (n + 1)));
A25: (NULL (#) seq) . n = NULL * (seq . n) by SEQ_1:9;
A26: (TWO (#) seq) . n = TWO * (seq . n) by SEQ_1:9;
A27: cl_Ball (p,(1 / (n + 1))) is bounded by TOPREAL6:59;
then A28: A /\ (cl_Ball (p,(1 / (n + 1)))) is bounded by TBSP_1:14, XBOOLE_1:17;
A29: diameter (A /\ (cl_Ball (p,(1 / (n + 1))))) <= diameter (cl_Ball (p,(1 / (n + 1)))) by A27, TBSP_1:24, XBOOLE_1:17;
diameter (cl_Ball (p,(1 / (n + 1)))) <= 2 * H₁(n) by Th5;
then A30: diameter (A /\ (cl_Ball (p,(1 / (n + 1))))) <= 2 * H₁(n) by A29, XXREAL_0:2;
n in NAT by ORDINAL1:def 12;
then A31: f . n = A /\ (cl_Ball (p,(1 / (n + 1)))) by A7;
then f . n is bounded by A28, Th15;
then A32: 0 <= diameter (f . n) by TBSP_1:21;
diameter (f . n) <= diameter (A /\ (cl_Ball (p,(1 / (n + 1))))) by A28, A31, Th16;
then A33: diameter (f . n) <= 2 * H₁(n) by A30, XXREAL_0:2;
H₁(n) = seq . n by A17;
hence ( (NULL (#) seq) . n <= (diameter f) . n & (diameter f) . n <= (TWO (#) seq) . n ) by A32, A33, A25, A26, Def2; :: thesis: verum

end;

A34: TWO (#) seq is convergent by A22, SEQ_2:7, SEQ_4:31;
A35: lim seq = 0 by A22, SEQ_4:31;
then A36: lim (TWO (#) seq) = TWO * 0 by A22, SEQ_2:8, SEQ_4:31;
lim (NULL (#) seq) = NULL * 0 by A22, A35, SEQ_2:8, SEQ_4:31;
then lim (diameter f) = 0 by A23, A34, A36, A24, SEQ_2:20;
then not meet f is empty by A3, A21, Th10;
then consider q being object such that
A37: q in meet f by XBOOLE_0:def 1;
reconsider q = q as Point of M by A37, TOPMETR:8;
A38: seq is convergent by A22, SEQ_4:31;
p = q

proof

assume p <> q ; :: thesis: contradiction
then dist (p,q) <> 0 by METRIC_1:2;
then dist (p,q) > 0 by METRIC_1:5;
then consider n being Nat such that
A39: for m being Nat st n <= m holds
|.((seq . m) - 0).| < dist (p,q) by A38, A35, SEQ_2:def 7;
set cB = cl_Ball (p,(1 / (n + 1)));
A40: q in f . n by A37, KURATO_0:3;
n in NAT by ORDINAL1:def 12;
then f . n = A /\ (cl_Ball (p,(1 / (n + 1)))) by A7;
then q in cl_Ball (p,(1 / (n + 1))) by A40, XBOOLE_0:def 4;
then A41: dist (p,q) <= H₁(n) by METRIC_1:12;
seq . n = H₁(n) by A17;
then |.((seq . n) - 0).| = H₁(n) by ABSVALUE:def 1;
hence contradiction by A39, A41; :: thesis: verum

end;

then A42: p in f . 0 by A37, KURATO_0:3;
f . 0 = A /\ (cl_Ball (p,(1 / (0 + 1)))) by A7;
hence p in A9 by A2, A42, XBOOLE_0:def 4; :: thesis: verum

end;

A9 c= Cl A9 by PRE_TOPC:18;
hence A9 is closed by A4, XBOOLE_0:def 10; :: thesis: verum

end;

assume A43: A9 is closed ; :: thesis: M | A is complete
let S be sequence of (M | A); :: according to TBSP_1:def 5 :: thesis: ( not S is Cauchy or S is convergent )
assume A44: S is Cauchy ; :: thesis: S is convergent
reconsider S9 = S as sequence of M by Th17;
S9 is Cauchy by A44, Th18;
then A45: S9 is convergent by A1;

A46: now :: thesis: for n being Nat holds S9 . n in A9

let n be Nat; :: thesis: S9 . n in A9
S . n in the carrier of (M | A) ;
hence S9 . n in A9 by A2, TOPMETR:def 2; :: thesis: verum

end;

the carrier of (M | A) = A9 by A2, TOPMETR:def 2;
then reconsider limS = lim S9 as Point of (M | A) by A43, A45, A46, TOPMETR3:1;
take limS ; :: 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 ((S . b₃),limS) ) )
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 ((S . b₂),limS) ) )
assume r > 0 ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not r <= dist ((S . b₂),limS) )
then consider n being Nat such that
A47: for m being Nat st m >= n holds
dist ((S9 . m),(lim S9)) < r by A45, TBSP_1:def 3;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or not r <= dist ((S . b₁),limS) )
let m be Nat; :: thesis: ( not n <= m or not r <= dist ((S . m),limS) )
assume A48: m >= n ; :: thesis: not r <= dist ((S . m),limS)
dist ((S . m),limS) = dist ((S9 . m),(lim S9)) by TOPMETR:def 1;
hence not r <= dist ((S . m),limS) by A47, A48; :: thesis: verum