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

end;

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

end;

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

end;

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;
dist (a,b) > 0 by A2, METRIC_1:5;
then A19: 2 * (dist (a,b)) > 0 by XREAL_1:129;
A20: rng S c= F

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng S ; :: thesis:
then consider y being object such that
A21: y in dom S and
A22: S . y = x by FUNCT_1:def 3;
dom s = NAT by FUNCT_2:def 1;
then A23: s . y in rngs by A21, FUNCT_1:def 3;
x = {(s . y)} by A10, A21, A22;
hence x in F by A23; :: thesis:

end;

end;

let x, y be Point of (WellSpace (a,X)); :: thesis:
assume that
A28: x in rngs and
A29: y in rngs and
A30: x <> y ; :: thesis:
consider y1 being object such that
A31: y1 in dom s and
A32: s . y1 = y by A29, FUNCT_1:def 3;
A33: y = [(f . y1),b] by A7, A31, A32;
consider x1 being object such that
A34: x1 in dom s and
A35: s . x1 = x by A28, FUNCT_1:def 3;
x = [(f . x1),b] by A7, A34, A35;
then (well_dist (a,X)) . (x,y) = (dist (b,a)) + (dist (a,b)) by A30, A33, Def10;
hence dist (x,y) = 2 * (dist (a,b)) ; :: thesis:

end;

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

let x, y be Point of (WellSpace (a,X)); :: thesis:
assume that
A38: x in SI and
A39: y in SI ; :: thesis:
consider xS being set such that
A40: x in xS and
A41: xS in Si by A38, TARSKI:def 4;
consider j1 being Element of NAT such that
A42: xS = S . j1 and
j1 >= i by A37, A41;
A43: S . j1 = {(s . j1)} by A10;
A44: dom s = NAT by FUNCT_2:def 1;
then s . j1 in rngs by FUNCT_1:def 3;
then A45: x in rngs by A40, A42, A43, TARSKI:def 1;
consider yS being set such that
A46: y in yS and
A47: yS in Si by A39, TARSKI:def 4;
consider j2 being Element of NAT such that
A48: yS = S . j2 and
j2 >= i by A37, A47;
A49: S . j2 = {(s . j2)} by A10;
s . j2 in rngs by A44, FUNCT_1:def 3;
then A50: y in rngs by A46, A48, A49, TARSKI:def 1;
( x = y or x <> y ) ;
hence dist (x,y) <= 2 * (dist (a,b)) by A19, A27, A45, A50, METRIC_1:1; :: thesis:

end;

end;

then reconsider R9 = R9 as non-empty pointwise_bounded SetSequence of (WellSpace (a,X)) by Def1;
take R9 ; :: thesis:
thus ( R9 is closed & R9 is non-ascending ) by A24, Th7; :: thesis:
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 A27;
hence meet R9 is empty by A25, A19, A11, Lm7, FUNCT_2:19; :: thesis: