let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis:
assume A1: M is complete ; :: thesis:
let a be Point of M; :: thesis:
assume A2: ex b being Point of M st dist a,b <> 0 ; :: thesis:
consider b being Point of M such that
A3: dist a,b <> 0 by A2;
A4: b <> a by A3, METRIC_1:1;
let X be infinite set ; :: thesis:
set W = WellSpace a,X;
thus WellSpace a,X is complete by A1, Th42; :: thesis:
set TW = TopSpaceMetr (WellSpace a,X);
consider f being Function of NAT ,X such that
A5: f is one-to-one by DICKSON:3;
defpred S₁[ set , set ] means $2 = [(f . $1),b];
A6: for x being set st x in NAT holds
ex y being set st
( y in the carrier of (TopSpaceMetr (WellSpace a,X)) & S₁[x,y] )

proof

let x be set ; :: thesis:
assume A7: x in NAT ; :: thesis:
take [(f . x),b] ; :: thesis:
x in dom f by A7, FUNCT_2:def 1;
then f . x in rng f by FUNCT_1:def 5;
hence ( [(f . x),b] in the carrier of (TopSpaceMetr (WellSpace a,X)) & S₁[x,[(f . x),b]] ) by A4, Th38; :: thesis:

end;

consider s being Function of NAT ,the carrier of (TopSpaceMetr (WellSpace a,X)) such that
A8: for x being set st x in NAT holds
S₁[x,s . x] from FUNCT_2:sch 1(A6);
deffunc H₁( set ) -> set = {(s . $1)};
A9: for x being set st x in NAT holds
H₁(x) in bool the carrier of (TopSpaceMetr (WellSpace a,X))

proof

let x be set ; :: thesis:
assume A10: x in NAT ; :: thesis:
dom s = NAT by FUNCT_2:def 1;
then s . x in rng s by A10, FUNCT_1:def 5;
then H₁(x) is Subset of (WellSpace a,X) by SUBSET_1:55;
hence H₁(x) in bool the carrier of (TopSpaceMetr (WellSpace a,X)) ; :: thesis:

end;

consider S being SetSequence of (TopSpaceMetr (WellSpace a,X)) such that
A11: for x being set st x in NAT holds
S . x = H₁(x) from FUNCT_2:sch 2(A9);

now

let x be set ; :: thesis:
assume A12: x in dom S ; :: thesis:
S . x = {(s . x)} by A11, A12;
hence not S . x is empty ; :: thesis:

end;

then A13: S is non-empty by FUNCT_1:def 15;
reconsider rngs = rng s as Subset of (TopSpaceMetr (WellSpace a,X)) ;
set F = { {x} where x is Element of (TopSpaceMetr (WellSpace a,X)) : x in rngs } ;
reconsider F = { {x} where x is Element of (TopSpaceMetr (WellSpace a,X)) : x in rngs } as Subset-Family of (TopSpaceMetr (WellSpace a,X)) by RELSET_2:16;
rng S c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A14: x in rng S ; :: thesis:
consider y being set such that
A15: ( y in dom S & S . y = x ) by A14, FUNCT_1:def 5;
( dom S = NAT & dom s = NAT ) by FUNCT_2:def 1;
then ( x = {(s . y)} & s . y in rngs ) by A11, A15, FUNCT_1:def 5;
hence x in F ; :: thesis:

end;

then consider R being non-empty closed SetSequence of (TopSpaceMetr (WellSpace a,X)) such that
A16: R is non-ascending and
A17: ( F is locally_finite & S is one-to-one implies meet R = {} ) and
A18: for i being natural number ex Si being Subset-Family of (TopSpaceMetr (WellSpace a,X)) st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) by A13, Th23;
reconsider R' = R as non-empty SetSequence of (WellSpace a,X) ;
dist a,b > 0 by A3, METRIC_1:5;
then A19: 2 * (dist a,b) > 0 by XREAL_1:131;

A20: now

let x, y be Point of (WellSpace a,X); :: thesis:
assume A21: ( x in rngs & y in rngs & x <> y ) ; :: thesis:
consider x1 being set such that
A22: ( x1 in dom s & s . x1 = x ) by A21, FUNCT_1:def 5;
consider y1 being set such that
A23: ( y1 in dom s & s . y1 = y ) by A21, FUNCT_1:def 5;
( x = [(f . x1),b] & y = [(f . y1),b] ) by A8, A22, A23;
then (well_dist a,X) . x,y = (dist b,a) + (dist a,b) by A21, Def10;
hence dist x,y = 2 * (dist a,b) ; :: thesis:

end;

now

let i be natural number ; :: thesis:
consider Si being Subset-Family of (TopSpaceMetr (WellSpace a,X)) such that
A24: R . i = Cl (union Si) and
A25: Si = { (S . j) where j is Element of NAT : j >= i } by A18;
reconsider SI = union Si as Subset of (WellSpace a,X) ;

now

let x, y be Point of (WellSpace a,X); :: thesis:
assume A26: ( x in SI & y in SI ) ; :: thesis:
consider xS being set such that
A27: ( x in xS & xS in Si ) by A26, TARSKI:def 4;
consider yS being set such that
A28: ( y in yS & yS in Si ) by A26, TARSKI:def 4;
consider j1 being Element of NAT such that
A29: ( xS = S . j1 & j1 >= i ) by A25, A27;
consider j2 being Element of NAT such that
A30: ( yS = S . j2 & j2 >= i ) by A25, A28;
( dom s = NAT & dom S = NAT ) by FUNCT_2:def 1;
then ( s . j1 in rngs & S . j1 = {(s . j1)} & s . j2 in rngs & S . j2 = {(s . j2)} ) by A11, FUNCT_1:def 5;
then ( x in rngs & y in rngs & ( x = y or x <> y ) ) by A27, A28, A29, A30, TARSKI:def 1;
hence dist x,y <= 2 * (dist a,b) by A19, A20, METRIC_1:1; :: thesis:

end;

then SI is bounded by A19, TBSP_1:def 9;
hence R' . i is bounded by A24, Th8; :: thesis:

end;

then reconsider R' = R' as non-empty bounded SetSequence of (WellSpace a,X) by Def1;
take R' ; :: thesis:
thus ( R' is closed & R' is non-ascending ) by A16, Th7; :: thesis:
A31: for x, y being Point of (WellSpace a,X) st x <> y & x in rngs & y in rngs holds
dist x,y >= 2 * (dist a,b) by A20;

now

let x1, x2 be set ; :: thesis:
assume A32: ( x1 in NAT & x2 in NAT & S . x1 = S . x2 ) ; :: thesis:
( S . x1 = {(s . x1)} & S . x2 = {(s . x2)} & s . x1 in {(s . x1)} ) by A11, A32, TARSKI:def 1;
then ( s . x1 = s . x2 & s . x1 = [(f . x1),b] & s . x2 = [(f . x2),b] ) by A8, A32, TARSKI:def 1;
then f . x1 = f . x2 by ZFMISC_1:33;
hence x1 = x2 by A5, A32, FUNCT_2:25; :: thesis:

end;

hence meet R' is empty by A17, A19, A31, Lm7, FUNCT_2:25; :: thesis: