:: Complete Spaces
:: by Karol P\c{a}k
::
:: Received October 12, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

definition
let M be non empty MetrStruct ;
let S be SetSequence of M;
attrS is pointwise_bounded  means :Def1: :: COMPL_SP:def 1
 for i being Nat holds S . i is bounded ;
end;

:: deftheorem Def1 defines pointwise_bounded COMPL_SP:def_1_:_
 for M being non empty MetrStruct
for S being SetSequence of M holds
( S is pointwise_bounded iff for i being Nat holds S . i is bounded );

registration
let M be non empty Reflexive MetrStruct ;
cluster non empty Relation-like non-empty NAT -defined bool the carrier of M -valued Function-like total V27( NAT , bool the carrier of M) pointwise_bounded for Element of bool [:NAT,(bool the carrier of M):];
existence
 ex b1 being SetSequence of M st
( b1 is pointwise_bounded & b1 is non-empty )
proofend;
end;

definition
let M be non empty Reflexive MetrStruct ;
let S be SetSequence of M;
func diameter S ->  Real_Sequence means :Def2: :: COMPL_SP:def 2
 for i being Nat holds it . i = diameter (S . i);
existence
 ex b1 being Real_Sequence st
for i being Nat holds b1 . i = diameter (S . i)
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = diameter (S . i) ) & ( for i being Nat holds b2 . i = diameter (S . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines diameter COMPL_SP:def_2_:_
 for M being non empty Reflexive MetrStruct
for S being SetSequence of M
for b3 being Real_Sequence holds
( b3 = diameter S iff for i being Nat holds b3 . i = diameter (S . i) );

theorem Th1: :: COMPL_SP:1
for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M holds diameter S is bounded_below
proofend;

theorem Th2: :: COMPL_SP:2
for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M st S is V172() holds
( diameter S is bounded_above & diameter S is V103() )
proofend;

theorem :: COMPL_SP:3
for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M st S is V173() holds
diameter S is V102()
proofend;

theorem Th4: :: COMPL_SP:4
for M being non empty Reflexive MetrStruct
for S being pointwise_bounded SetSequence of M st S is V172() & lim (diameter S) = 0 holds
for F being sequence of M st ( for i being Nat holds F . i in S . i ) holds
F is Cauchy
proofend;

theorem Th5: :: COMPL_SP:5
for r being Real
for M being non empty Reflexive symmetric triangle MetrStruct
for p being Point of M st 0 <= r holds
diameter (cl_Ball (p,r)) <= 2 * r
proofend;

definition
let M be MetrStruct ;
let U be Subset of M;
attrU is open  means :Def3: :: COMPL_SP:def 3
U in Family_open_set M;
end;

:: deftheorem Def3 defines open COMPL_SP:def_3_:_
 for M being MetrStruct
for U being Subset of M holds
( U is open iff U in Family_open_set M );

definition
let M be MetrStruct ;
let A be Subset of M;
attrA is closed  means :Def4: :: COMPL_SP:def 4
A ` is open ;
end;

:: deftheorem Def4 defines closed COMPL_SP:def_4_:_
 for M being MetrStruct
for A being Subset of M holds
( A is closed iff A ` is open );

registration
let M be MetrStruct ;
cluster empty  ->  open for Element of bool the carrier of M;
coherence
 for b1 being Subset of M st b1 is empty holds
b1 is open
proofend;
cluster empty  ->  closed for Element of bool the carrier of M;
coherence
 for b1 being Subset of M st b1 is empty holds
b1 is closed
proofend;
end;

registration
let M be non empty MetrStruct ;
cluster non empty open for Element of bool the carrier of M;
existence
 ex b1 being Subset of M st
( b1 is open &amp; not b1 is empty )
proofend;
cluster non empty closed for Element of bool the carrier of M;
existence
 ex b1 being Subset of M st
( b1 is closed &amp; not b1 is empty )
proofend;
end;

theorem Th6: :: COMPL_SP:6
for M being MetrStruct
for A being Subset of M
for A9 being Subset of (TopSpaceMetr M) st A9 = A holds
( ( A is open implies A9 is open ) &amp; ( A9 is open implies A is open ) &amp; ( A is closed implies A9 is closed ) &amp; ( A9 is closed implies A is closed ) )
proofend;

definition
let T be TopStruct ;
let S be SetSequence of T;
attrS is open  means :Def5: :: COMPL_SP:def 5
 for i being Nat holds S . i is open ;
attrS is closed  means :Def6: :: COMPL_SP:def 6
 for i being Nat holds S . i is closed ;
end;

:: deftheorem Def5 defines open COMPL_SP:def_5_:_
 for T being TopStruct
for S being SetSequence of T holds
( S is open iff for i being Nat holds S . i is open );

:: deftheorem Def6 defines closed COMPL_SP:def_6_:_
 for T being TopStruct
for S being SetSequence of T holds
( S is closed iff for i being Nat holds S . i is closed );

Lm1:  for T being TopSpace ex S being SetSequence of T st
( S is open &amp; S is closed &amp; ( not T is empty implies S is non-empty ) )
proofend;

registration
let T be TopSpace;
cluster non empty Relation-like NAT -defined bool the carrier of T -valued Function-like total V27( NAT , bool the carrier of T) open for Element of bool [:NAT,(bool the carrier of T):];
existence
 ex b1 being SetSequence of T st b1 is open
proofend;
cluster non empty Relation-like NAT -defined bool the carrier of T -valued Function-like total V27( NAT , bool the carrier of T) closed for Element of bool [:NAT,(bool the carrier of T):];
existence
 ex b1 being SetSequence of T st b1 is closed
proofend;
end;

registration
let T be non empty TopSpace;
cluster non empty Relation-like non-empty NAT -defined bool the carrier of T -valued Function-like total V27( NAT , bool the carrier of T) open for Element of bool [:NAT,(bool the carrier of T):];
existence
 ex b1 being SetSequence of T st
( b1 is open &amp; b1 is non-empty )
proofend;
cluster non empty Relation-like non-empty NAT -defined bool the carrier of T -valued Function-like total V27( NAT , bool the carrier of T) closed for Element of bool [:NAT,(bool the carrier of T):];
existence
 ex b1 being SetSequence of T st
( b1 is closed &amp; b1 is non-empty )
proofend;
end;

definition
let M be MetrStruct ;
let S be SetSequence of M;
attrS is open  means :Def7: :: COMPL_SP:def 7
 for i being Nat holds S . i is open ;
attrS is closed  means :Def8: :: COMPL_SP:def 8
 for i being Nat holds S . i is closed ;
end;

:: deftheorem Def7 defines open COMPL_SP:def_7_:_
 for M being MetrStruct
for S being SetSequence of M holds
( S is open iff for i being Nat holds S . i is open );

:: deftheorem Def8 defines closed COMPL_SP:def_8_:_
 for M being MetrStruct
for S being SetSequence of M holds
( S is closed iff for i being Nat holds S . i is closed );

registration
let M be non empty MetrSpace;
cluster non empty Relation-like non-empty NAT -defined bool the carrier of M -valued Function-like total V27( NAT , bool the carrier of M) pointwise_bounded open for Element of bool [:NAT,(bool the carrier of M):];
existence
 ex b1 being SetSequence of M st
( b1 is non-empty &amp; b1 is pointwise_bounded &amp; b1 is open )
proofend;
cluster non empty Relation-like non-empty NAT -defined bool the carrier of M -valued Function-like total V27( NAT , bool the carrier of M) pointwise_bounded closed for Element of bool [:NAT,(bool the carrier of M):];
existence
 ex b1 being SetSequence of M st
( b1 is non-empty &amp; b1 is pointwise_bounded &amp; b1 is closed )
proofend;
end;

theorem Th7: :: COMPL_SP:7
for M being MetrStruct
for S being SetSequence of M
for S9 being SetSequence of (TopSpaceMetr M) st S9 = S holds
( ( S is open implies S9 is open ) &amp; ( S9 is open implies S is open ) &amp; ( S is closed implies S9 is closed ) &amp; ( S9 is closed implies S is closed ) )
proofend;

theorem Th8: :: COMPL_SP:8
for M being non empty Reflexive symmetric triangle MetrStruct
for S, CL being Subset of M st S is bounded holds
for S9 being Subset of (TopSpaceMetr M) st S = S9 &amp; CL = Cl S9 holds
( CL is bounded &amp; diameter S = diameter CL )
proofend;

begin

theorem Th9: :: COMPL_SP:9
for M being non empty MetrSpace
for C being sequence of M ex S being non-empty closed SetSequence of M st
( S is V172() &amp; ( C is Cauchy implies ( S is pointwise_bounded &amp; lim (diameter S) = 0 ) ) &amp; ( for i being Nat ex U being Subset of (TopSpaceMetr M) st
( U =  {  (C . j) where j is Element of NAT : j >= i  }  &amp; S . i = Cl U ) ) )
proofend;

theorem Th10: :: COMPL_SP:10
for M being non empty MetrSpace holds
( M is complete iff for S being non-empty pointwise_bounded closed SetSequence of M st S is V172() &amp; lim (diameter S) = 0 holds
not meet S is empty )
proofend;

theorem Th11: :: COMPL_SP:11
for T being non empty TopSpace
for S being non-empty SetSequence of T st S is V172() holds
for F being Subset-Family of T st F = rng S holds
F is centered
proofend;

theorem Th12: :: COMPL_SP:12
for M being non empty MetrStruct
for S being SetSequence of M
for F being Subset-Family of (TopSpaceMetr M) st F = rng S holds
( ( S is open implies F is open ) &amp; ( S is closed implies F is closed ) )
proofend;

theorem Th13: :: COMPL_SP:13
for T being non empty TopSpace
for F being Subset-Family of T
for S being SetSequence of T st rng S c= F holds
ex R being SetSequence of T st
( R is V172() &amp; ( F is centered implies R is non-empty ) &amp; ( F is open implies R is open ) &amp; ( F is closed implies R is closed ) &amp; ( for i being Nat holds R . i = meet  {  (S . j) where j is Element of NAT : j <= i  }  ) )
proofend;

theorem :: COMPL_SP:14
for M being non empty MetrSpace holds
( M is complete iff for F being Subset-Family of (TopSpaceMetr M) st F is closed &amp; F is centered &amp; ( for r being Real st r > 0 holds
ex A being Subset of M st
( A in F &amp; A is bounded &amp; diameter A < r ) ) holds
not meet F is empty )
proofend;

theorem Th15: :: COMPL_SP:15
for M being non empty MetrSpace
for A being non empty Subset of M
for B being Subset of M
for B9 being Subset of (M | A) st B = B9 holds
( B9 is bounded iff B is bounded )
proofend;

theorem Th16: :: COMPL_SP:16
for M being non empty MetrSpace
for A being non empty Subset of M
for B being Subset of M
for B9 being Subset of (M | A) st B = B9 &amp; B is bounded holds
diameter B9 <= diameter B
proofend;

theorem Th17: :: COMPL_SP:17
for M being non empty MetrSpace
for A being non empty Subset of M
for S being sequence of (M | A) holds S is sequence of M
proofend;

theorem Th18: :: COMPL_SP:18
for M being non empty MetrSpace
for A being non empty Subset of M
for S being sequence of (M | A)
for S9 being sequence of M st S = S9 holds
( S9 is Cauchy iff S is Cauchy )
proofend;

theorem :: COMPL_SP:19
for M being non empty MetrSpace st M is complete holds
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 )
proofend;

begin

definition
let T be TopStruct ;
attrT is countably_compact  means :Def9: :: COMPL_SP:def 9
 for F being Subset-Family of T st F is Cover of T &amp; F is open &amp; F is countable holds
ex G being Subset-Family of T st
( G c= F &amp; G is Cover of T &amp; G is finite );
end;

:: deftheorem Def9 defines countably_compact COMPL_SP:def_9_:_
 for T being TopStruct holds
( T is countably_compact iff for F being Subset-Family of T st F is Cover of T &amp; F is open &amp; F is countable holds
ex G being Subset-Family of T st
( G c= F &amp; G is Cover of T &amp; G is finite ) );

theorem Th20: :: COMPL_SP:20
for T being TopStruct st T is compact holds
T is countably_compact
proofend;

theorem Th21: :: COMPL_SP:21
for T being non empty TopSpace holds
( T is countably_compact iff for F being Subset-Family of T st F is centered &amp; F is closed &amp; F is countable holds
meet F <> {} )
proofend;

theorem Th22: :: COMPL_SP:22
for T being non empty TopSpace holds
( T is countably_compact iff for S being non-empty closed SetSequence of T st S is V172() holds
meet S <> {} )
proofend;

theorem Th23: :: COMPL_SP:23
for T being non empty TopSpace
for F being Subset-Family of T
for S being SetSequence of T st rng S c= F &amp; S is non-empty holds
ex R being non-empty closed SetSequence of T st
( R is V172() &amp; ( F is locally_finite &amp; S is one-to-one implies meet R = {} ) &amp; ( for i being Nat ex Si being Subset-Family of T st
( R . i = Cl (union Si) &amp; Si =  {  (S . j) where j is Element of NAT : j >= i  }  ) ) )
proofend;

Lm2:  for T being non empty TopSpace st T is countably_compact holds
for F being Subset-Family of T st F is locally_finite &amp; F is with_non-empty_elements holds
F is finite
proofend;

Lm3:  for T being non empty TopSpace st ( for F being Subset-Family of T st F is locally_finite &amp; F is with_non-empty_elements holds
F is finite ) holds
for F being Subset-Family of T st F is locally_finite &amp; ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite
proofend;

Lm4:  for T being non empty TopSpace st ( for F being Subset-Family of T st F is locally_finite &amp; ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite ) holds
for A being Subset of T st A is infinite holds
not Der A is empty
proofend;

theorem :: COMPL_SP:24
canceled;

theorem Th25: :: COMPL_SP:25
for X being non empty set
for F being SetSequence of X st F is V172() holds
for S being Function of NAT,X st ( for n being Nat holds S . n in F . n ) &amp; rng S is finite holds
not meet F is empty
proofend;

Lm5:  for T being non empty T_1 TopSpace st ( for A being Subset of T st A is infinite &amp; A is countable holds
not Der A is empty ) holds
T is countably_compact
proofend;

Lm6:  for T being non empty TopSpace st ( for F being Subset-Family of T st F is locally_finite &amp; ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite ) holds
T is countably_compact
proofend;

theorem Th26: :: COMPL_SP:26
for T being non empty TopSpace holds
( T is countably_compact iff for F being Subset-Family of T st F is locally_finite &amp; F is with_non-empty_elements holds
F is finite )
proofend;

theorem Th27: :: COMPL_SP:27
for T being non empty TopSpace holds
( T is countably_compact iff for F being Subset-Family of T st F is locally_finite &amp; ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite )
proofend;

theorem Th28: :: COMPL_SP:28
for T being non empty T_1 TopSpace holds
( T is countably_compact iff for A being Subset of T st A is infinite holds
not Der A is empty )
proofend;

theorem :: COMPL_SP:29
for T being non empty T_1 TopSpace holds
( T is countably_compact iff for A being Subset of T st A is infinite &amp; A is countable holds
not Der A is empty ) by Lm5, Th28;

scheme :: COMPL_SP:sch 1
Th39{ F1() ->  non empty set , P1[ set , set ] } :
 ex A being Subset of F1() st
( ( for x, y being Element of F1() st x in A &amp; y in A &amp; x <> y holds
P1[x,y] ) &amp; ( for x being Element of F1() ex y being Element of F1() st
( y in A &amp; P1[x,y] ) ) )
provided
A1: for x, y being Element of F1() holds
( P1[x,y] iff P1[y,x] ) and
A2: for x being Element of F1() holds P1[x,x]
proofend;

theorem Th30: :: COMPL_SP:30
for M being non empty Reflexive symmetric MetrStruct
for r being Real st r > 0 holds
ex A being Subset of M st
( ( for p, q being Point of M st p <> q &amp; p in A &amp; q in A holds
dist (p,q) >= r ) &amp; ( for p being Point of M ex q being Point of M st
( q in A &amp; p in Ball (q,r) ) ) )
proofend;

theorem Th31: :: COMPL_SP:31
for M being non empty Reflexive symmetric triangle MetrStruct holds
( M is totally_bounded iff for r being Real
for A being Subset of M st r > 0 &amp; ( for p, q being Point of M st p <> q &amp; p in A &amp; q in A holds
dist (p,q) >= r ) holds
A is finite )
proofend;

Lm7:  for M being non empty Reflexive symmetric triangle MetrStruct
for r being Real
for A being Subset of M st r > 0 &amp; ( for p, q being Point of M st p <> q &amp; p in A &amp; q in A holds
dist (p,q) >= r ) holds
for F being Subset-Family of (TopSpaceMetr M) st F =  {  {x} where x is Element of (TopSpaceMetr M) : x in A  }  holds
F is locally_finite
proofend;

theorem Th32: :: COMPL_SP:32
for M being non empty Reflexive symmetric triangle MetrStruct st TopSpaceMetr M is countably_compact holds
M is totally_bounded
proofend;

theorem Th33: :: COMPL_SP:33
for M being non empty MetrSpace st M is totally_bounded holds
TopSpaceMetr M is second-countable
proofend;

theorem Th34: :: COMPL_SP:34
for T being non empty TopSpace st T is second-countable holds
for F being Subset-Family of T st F is Cover of T &amp; F is open holds
ex G being Subset-Family of T st
( G c= F &amp; G is Cover of T &amp; G is countable )
proofend;

begin

theorem Th35: :: COMPL_SP:35
for M being non empty MetrSpace holds
( TopSpaceMetr M is compact iff TopSpaceMetr M is countably_compact )
proofend;

theorem Th36: :: COMPL_SP:36
for X being set
for F being Subset-Family of X st F is finite holds
for A being Subset of X st A is infinite &amp; A c= union F holds
ex Y being Subset of X st
( Y in F &amp; Y /\ A is infinite )
proofend;

theorem :: COMPL_SP:37
for M being non empty MetrSpace holds
( TopSpaceMetr M is compact iff ( M is totally_bounded &amp; M is complete ) )
proofend;

begin

theorem Th38: :: COMPL_SP:38
for X being set
for M being MetrStruct
for a being Point of M
for x being set holds
( x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} iff ex y being set ex b being Point of M st
( x = [y,b] &amp; ( ( y in X &amp; b <> a ) or ( y = X &amp; b = a ) ) ) )
proofend;

definition
let M be MetrStruct ;
let a be Point of M;
let X be set ;
func well_dist (a,X) ->  Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL means :Def10: :: COMPL_SP:def 10
 for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being set
for x2, y2 being Point of M st x = [x1,x2] &amp; y = [y1,y2] holds
( ( x1 = y1 implies it . (x,y) = dist (x2,y2) ) &amp; ( x1 <> y1 implies it . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) );
existence
 ex b1 being Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL st
for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being set
for x2, y2 being Point of M st x = [x1,x2] &amp; y = [y1,y2] holds
( ( x1 = y1 implies b1 . (x,y) = dist (x2,y2) ) &amp; ( x1 <> y1 implies b1 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) )
proofend;
uniqueness
 for b1, b2 being Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL st ( for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being set
for x2, y2 being Point of M st x = [x1,x2] &amp; y = [y1,y2] holds
( ( x1 = y1 implies b1 . (x,y) = dist (x2,y2) ) &amp; ( x1 <> y1 implies b1 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) ) &amp; ( for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being set
for x2, y2 being Point of M st x = [x1,x2] &amp; y = [y1,y2] holds
( ( x1 = y1 implies b2 . (x,y) = dist (x2,y2) ) &amp; ( x1 <> y1 implies b2 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines well_dist COMPL_SP:def_10_:_
 for M being MetrStruct
for a being Point of M
for X being set
for b4 being Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL holds
( b4 = well_dist (a,X) iff for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being set
for x2, y2 being Point of M st x = [x1,x2] &amp; y = [y1,y2] holds
( ( x1 = y1 implies b4 . (x,y) = dist (x2,y2) ) &amp; ( x1 <> y1 implies b4 . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) );

theorem :: COMPL_SP:39
for M being MetrStruct
for a being Point of M
for X being non empty set holds
( ( well_dist (a,X) is Reflexive implies M is Reflexive ) &amp; ( well_dist (a,X) is symmetric implies M is symmetric ) &amp; ( well_dist (a,X) is triangle &amp; well_dist (a,X) is Reflexive implies M is triangle ) &amp; ( well_dist (a,X) is discerning &amp; well_dist (a,X) is Reflexive implies M is discerning ) )
proofend;

definition
let M be MetrStruct ;
let a be Point of M;
let X be set ;
func WellSpace (a,X) ->  strict MetrStruct  equals :: COMPL_SP:def 11
 MetrStruct(# ([:X,( the carrier of M \ {a}):] \/ {[X,a]}),(well_dist (a,X)) #);
coherence
 MetrStruct(# ([:X,( the carrier of M \ {a}):] \/ {[X,a]}),(well_dist (a,X)) #) is strict MetrStruct ;
end;

:: deftheorem  defines WellSpace COMPL_SP:def_11_:_
 for M being MetrStruct
for a being Point of M
for X being set holds WellSpace (a,X) = MetrStruct(# ([:X,( the carrier of M \ {a}):] \/ {[X,a]}),(well_dist (a,X)) #);

registration
let M be MetrStruct ;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) ->  non empty strict ;
coherence
 not WellSpace (a,X) is empty ;
end;

Lm8:  for M being MetrStruct
for a being Point of M
for X being set holds
( ( M is Reflexive implies WellSpace (a,X) is Reflexive ) &amp; ( M is symmetric implies WellSpace (a,X) is symmetric ) &amp; ( M is triangle &amp; M is symmetric &amp; M is Reflexive implies WellSpace (a,X) is triangle ) &amp; ( M is triangle &amp; M is symmetric &amp; M is Reflexive &amp; M is discerning implies WellSpace (a,X) is discerning ) )
proofend;

registration
let M be Reflexive MetrStruct ;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) ->  strict Reflexive ;
coherence
 WellSpace (a,X) is Reflexive by Lm8;
end;

registration
let M be symmetric MetrStruct ;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) ->  strict symmetric ;
coherence
 WellSpace (a,X) is symmetric by Lm8;
end;

registration
let M be Reflexive symmetric triangle MetrStruct ;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) ->  strict triangle ;
coherence
 WellSpace (a,X) is triangle by Lm8;
end;

registration
let M be MetrSpace;
let a be Point of M;
let X be set ;
cluster WellSpace (a,X) ->  strict discerning ;
coherence
 WellSpace (a,X) is discerning by Lm8;
end;

theorem :: COMPL_SP:40
for M being non empty Reflexive triangle MetrStruct
for a being Point of M
for X being non empty set st WellSpace (a,X) is complete holds
M is complete
proofend;

theorem Th41: :: COMPL_SP:41
for X being set
for M being non empty Reflexive symmetric triangle MetrStruct
for a being Point of M
for S being sequence of (WellSpace (a,X)) holds
( not S is Cauchy or for Xa being Point of (WellSpace (a,X)) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat st m >= n holds
ex p being Point of M st S . m = [Y,p] )
proofend;

theorem Th42: :: COMPL_SP:42
for X being set
for M being non empty Reflexive symmetric triangle MetrStruct
for a being Point of M st M is complete holds
WellSpace (a,X) is complete
proofend;

theorem Th43: :: COMPL_SP:43
for M being non empty Reflexive symmetric triangle MetrStruct st M is complete holds
for a being Point of M st ex b being Point of M st dist (a,b) <> 0 holds
for X being infinite set holds
( WellSpace (a,X) is complete &amp; ex S being non-empty pointwise_bounded SetSequence of (WellSpace (a,X)) st
( S is closed &amp; S is V172() &amp; meet S is empty ) )
proofend;

theorem :: COMPL_SP:44
ex M being non empty MetrSpace st
( M is complete &amp; ex S being non-empty pointwise_bounded SetSequence of M st
( S is closed &amp; S is V172() &amp; meet S is empty ) )
proofend;