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

proof

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

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in Cl A' or p in A' )
assume A5: p in Cl A' ; :: thesis: p in A'
reconsider p = p as Point of M by A5;
defpred S₁[ set , set ] means for i being natural number st i = $1 holds
$2 = A /\ (cl_Ball p,(1 / (i + 1)));
A6: for x being set st x in NAT holds
ex y being set st
( y in bool the carrier of (M | A) & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in bool the carrier of (M | A) & S₁[x,y] ) )
assume A7: x in NAT ; :: thesis: ex y being set st
( y in bool the carrier of (M | A) & S₁[x,y] )
reconsider i = x as Element of NAT by A7;
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
A8: for x being set st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A6);

A9: now

let x be set ; :: thesis: ( x in dom f implies not f . x is empty )
assume A10: x in dom f ; :: thesis: not f . x is empty
reconsider i = x as Element of NAT by A10;
reconsider B = Ball p,(1 / (i + 1)) as Subset of (TopSpaceMetr M) ;
( Ball p,(1 / (i + 1)) in Family_open_set M & 1 / (i + 1) > 0 ) by PCOMPS_1:33, XREAL_1:141;
then ( B is open & p in B ) by PRE_TOPC:def 5, TBSP_1:16;
then B meets A' by A5, PRE_TOPC:54;
then consider y being set such that
A11: ( y in B & y in A' ) by XBOOLE_0:3;
reconsider y = y as Point of M by A11;
dist p,y < 1 / (i + 1) by A11, METRIC_1:12;
then y in cl_Ball p,(1 / (i + 1)) by METRIC_1:13;
then y in A /\ (cl_Ball p,(1 / (i + 1))) by A2, A11, XBOOLE_0:def 4;
hence not f . x is empty by A8; :: thesis: verum

end;

A12: now

let i be natural number ; :: thesis: f . i is bounded
set ACL = A /\ (cl_Ball p,(1 / (i + 1)));
( cl_Ball p,(1 / (i + 1)) is bounded & A /\ (cl_Ball p,(1 / (i + 1))) c= cl_Ball p,(1 / (i + 1)) ) by TOPREAL6:67, XBOOLE_1:17;
then A13: A /\ (cl_Ball p,(1 / (i + 1))) is bounded by TBSP_1:21;
i in NAT by ORDINAL1:def 13;
then f . i = A /\ (cl_Ball p,(1 / (i + 1))) by A8;
hence f . i is bounded by A13, Th15; :: thesis: verum

end;

now

let i be natural number ; :: thesis: f . i is closed
reconsider cB = cl_Ball p,(1 / (i + 1)) as Subset of (TopSpaceMetr M) ;
( cB ` = ([#] M) \ cB & ([#] M) \ cB in Family_open_set M ) by NAGATA_1:14;
then cB ` is open by PRE_TOPC:def 5;
then A14: cB is closed by TOPS_1:29;
reconsider fi = f . i as Subset of (TopSpaceMetr (M | A)) ;
A15: TopSpaceMetr (M | A) = (TopSpaceMetr M) | A' by A2, HAUSDORF:18;
then ( [#] ((TopSpaceMetr M) | A') = A & i in NAT ) by ORDINAL1:def 13, TOPMETR:def 2;
then fi = cB /\ ([#] ((TopSpaceMetr M) | A')) by A8;
then fi is closed by A14, A15, PRE_TOPC:43;
hence f . i is closed by Th6; :: thesis: verum

end;

then reconsider f = f as non-empty bounded closed SetSequence of (M | A) by A9, A12, Def1, Def8, FUNCT_1:def 15;

now

let i be Element of 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 set ; :: 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 A16: 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 A16;
i + 1 < (i + 1) + 1 by NAT_1:13;
then ( dist p,q <= 1 / ((i + 1) + 1) & 1 / ((i + 1) + 1) < 1 / (i + 1) ) by A16, METRIC_1:13, XREAL_1:78;
then dist p,q <= 1 / (i + 1) by XXREAL_0:2;
hence x in cl_Ball p,(1 / (i + 1)) by METRIC_1:13; :: thesis: verum

end;

then ( A /\ (cl_Ball p,(1 / ((i + 1) + 1))) c= A /\ (cl_Ball p,(1 / (i + 1))) & f . i = A /\ (cl_Ball p,(1 / (i + 1))) ) by A8, XBOOLE_1:26;
hence f . (i + 1) c= f . i by A8; :: thesis: verum

end;

then A17: f is non-ascending by KURATO_2:def 5;
deffunc H₁( Element of NAT ) -> Element of REAL = 1 / (1 + $1);
consider seq being Real_Sequence such that
A18: for n being Element of NAT holds seq . n = H₁(n) from SEQ_1:sch 1();
reconsider NULL = 0 , TWO = 2 as Real ;
set Ns = NULL (#) seq;
set Ts = TWO (#) seq;
for n being Element of NAT holds seq . n = 1 / (n + 1) by A18;
then A19: ( seq is convergent & lim seq = 0 ) by SEQ_4:45;
then A20: ( NULL (#) seq is convergent & lim (NULL (#) seq) = NULL * 0 & TWO (#) seq is convergent & lim (TWO (#) seq) = TWO * 0 ) by SEQ_2:21, SEQ_2:22;
set df = diameter f;

now

let n be Element of NAT ; :: thesis: ( (NULL (#) seq) . n <= (diameter f) . n & (diameter f) . n <= (TWO (#) seq) . n )
set cB = cl_Ball p,(1 / (n + 1));
A21: ( cl_Ball p,(1 / (n + 1)) is bounded & diameter (cl_Ball p,(1 / (n + 1))) <= 2 * H₁(n) & A /\ (cl_Ball p,(1 / (n + 1))) c= cl_Ball p,(1 / (n + 1)) ) by Th5, TOPREAL6:67, XBOOLE_1:17;
then ( A /\ (cl_Ball p,(1 / (n + 1))) is bounded & diameter (A /\ (cl_Ball p,(1 / (n + 1)))) <= diameter (cl_Ball p,(1 / (n + 1))) & f . n = A /\ (cl_Ball p,(1 / (n + 1))) ) by A8, TBSP_1:21, TBSP_1:32;
then ( diameter (A /\ (cl_Ball p,(1 / (n + 1)))) <= 2 * H₁(n) & diameter (f . n) <= diameter (A /\ (cl_Ball p,(1 / (n + 1)))) & f . n is bounded ) by A21, Th15, Th16, XXREAL_0:2;
then ( 0 <= diameter (f . n) & diameter (f . n) <= 2 * H₁(n) & (NULL (#) seq) . n = NULL * (seq . n) & (TWO (#) seq) . n = TWO * (seq . n) & H₁(n) = seq . n & diameter (f . n) = (diameter f) . n ) by A18, Def2, SEQ_1:13, TBSP_1:29, XXREAL_0:2;
hence ( (NULL (#) seq) . n <= (diameter f) . n & (diameter f) . n <= (TWO (#) seq) . n ) ; :: thesis: verum

end;

then ( lim (diameter f) = 0 & diameter f is convergent ) by A20, SEQ_2:33, SEQ_2:34;
then not meet f is empty by A3, A17, Th10;
then consider q being set such that
A22: q in meet f by XBOOLE_0:def 1;
reconsider q = q as Point of M by A22, TOPMETR:12;
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 Element of NAT such that
A23: for m being Element of NAT st n <= m holds
abs ((seq . m) - 0 ) < dist p,q by A19, SEQ_2:def 7;
set cB = cl_Ball p,(1 / (n + 1));
( f . n = A /\ (cl_Ball p,(1 / (n + 1))) & q in f . n & seq . n = H₁(n) & H₁(n) >= 0 ) by A8, A18, A22, KURATO_2:6;
then ( q in cl_Ball p,(1 / (n + 1)) & abs ((seq . n) - 0 ) = H₁(n) ) by ABSVALUE:def 1, XBOOLE_0:def 4;
then ( dist p,q <= H₁(n) & H₁(n) < dist p,q ) by A23, METRIC_1:13;
hence contradiction ; :: thesis: verum

end;

then ( f . 0 = A /\ (cl_Ball p,(1 / (0 + 1))) & p in f . 0 ) by A8, A22, KURATO_2:6;
hence p in A' by A2, XBOOLE_0:def 4; :: thesis: verum

end;

A' c= Cl A' by PRE_TOPC:48;
hence A' is closed by A4, XBOOLE_0:def 10; :: thesis: verum

end;

assume A24: A' is closed ; :: thesis: M | A is complete
let S be sequence of (M | A); :: according to TBSP_1:def 6 :: thesis: ( not S is Cauchy or S is convergent )
assume A25: S is Cauchy ; :: thesis: S is convergent
reconsider S' = S as sequence of M by Th17;
S' is Cauchy by A25, Th18;
then A26: S' is convergent by A1, TBSP_1:def 6;
A27: the carrier of (M | A) = A' by A2, TOPMETR:def 2;

now

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

end;

then reconsider limS = lim S' as Point of (M | A) by A24, A26, A27, TOPMETR3:2;
take limS ; :: 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 (S . b₃),limS ) )
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 (S . b₂),limS ) )
assume A28: r > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not r <= dist (S . b₂),limS )
consider n being Element of NAT such that
A29: for m being Element of NAT st m >= n holds
dist (S' . m),(lim S') < r by A26, A28, TBSP_1:def 4;
take n ; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not r <= dist (S . b₁),limS )
let m be Element of NAT ; :: thesis: ( not n <= m or not r <= dist (S . m),limS )
assume A30: m >= n ; :: thesis: not r <= dist (S . m),limS
dist (S . m),limS = dist (S' . m),(lim S') by TOPMETR:def 1;
hence not r <= dist (S . m),limS by A29, A30; :: thesis: verum