let T be non empty TopSpace; :: thesis:
set cT = the carrier of T;
assume T is metrizable ; :: thesis:
then consider metr being Function of [:the carrier of T,the carrier of T:],REAL such that
A1: metr is_metric_of the carrier of T and
A2: Family_open_set (SpaceMetr the carrier of T,metr) = the topology of T by PCOMPS_1:def 9;
reconsider PM = SpaceMetr the carrier of T,metr as non empty MetrSpace by PCOMPS_1:40, A1;
set cPM = the carrier of PM;
let FX be Subset-Family of T; :: thesis:
assume that
A3: FX is Cover of T and
A4: FX is open ; :: thesis:
consider R being Relation such that
A5: R well_orders FX by WELLORD2:26;
consider Mn being Relation such that
A6: Mn = R |_2 FX ;
set UB = { (union { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ) where V is Subset of PM : V in FX } ;
{ (union { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ) where V is Subset of PM : V in FX } c= bool the carrier of PM

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (union { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ) where V is Subset of PM : V in FX } ; :: thesis:
then consider V being Subset of PM such that
A7: x = union { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } and
V in FX ;
x c= the carrier of PM

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in x ; :: thesis:
then consider W being set such that
A8: ( y in W & W in { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ) by A7, TARSKI:def 4;
ex c being Point of PM st
( W = Ball c,(1 / 2) & c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) by A8;
hence y in the carrier of PM by A8; :: thesis:

end;

hence x in bool the carrier of PM ; :: thesis:

end;

then reconsider UB = { (union { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ) where V is Subset of PM : V in FX } as Subset-Family of PM ;
deffunc H₁( Point of PM, Nat) -> Element of bool the carrier of PM = Ball $1,(1 / (2 |^ ($2 + 1)));
defpred S₁[ Point of PM, Subset of PM, Nat] means ( $1 in $2 \ (PartUnion $2,Mn) & Ball $1,(3 / (2 |^ ($3 + 1))) c= $2 );
defpred S₂[ set ] means $1 in FX;
consider Un being Function of NAT ,(bool (bool the carrier of PM)) such that
A9: ( Un . 0 = UB & ( for n being Element of NAT holds Un . (n + 1) = { (union { H₁(c,n) where c is Point of PM : ( S₁[c,V,n] & not c in union { (union (Un . k)) where k is Element of NAT : k <= n } ) } ) where V is Subset of PM : S₂[V] } ) ) from PCOMPS_2:sch 3();
the carrier of T = the carrier of PM by A1, PCOMPS_2:8;
then reconsider Un' = Un as FamilySequence of T ;
take Un' ; :: thesis:
thus Union Un' is open :: thesis:

proof

let A be Subset of T; :: according to TOPS_2:def 1 :: thesis:
assume A in Union Un' ; :: thesis:
then consider n being Element of NAT such that
A10: A in Un . n by PROB_1:25;

per cases ;

suppose n = 0 ; :: thesis:

then consider V being Subset of PM such that
A11: A = union { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } and
V in FX by A9, A10;
set BALL = { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ;
{ (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } c= bool the carrier of PM

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ; :: thesis:
then ex c being Point of PM st
( x = Ball c,(1 / 2) & c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) ;
hence x in bool the carrier of PM ; :: thesis:

end;

then reconsider BALL = { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } as Subset-Family of PM ;
BALL c= Family_open_set PM

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in BALL ; :: thesis:
then ex c being Point of PM st
( x = Ball c,(1 / 2) & c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) ;
hence x in Family_open_set PM by PCOMPS_1:33; :: thesis:

end;

then A in the topology of T by A2, A11, PCOMPS_1:36;
hence A is open by PRE_TOPC:def 5; :: thesis:

end;

suppose n > 0 ; :: thesis:

then consider m being Nat such that
A12: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A in { (union { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) where V is Subset of PM : S₂[V] } by A9, A10, A12;
then consider V being Subset of PM such that
A13: ( A = union { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } & S₂[V] ) ;
set BALL = { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ;
{ H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } c= bool the carrier of PM

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ; :: thesis:
then ex c being Point of PM st
( x = H₁(c,m) & S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) ;
hence x in bool the carrier of PM ; :: thesis:

end;

then reconsider BALL = { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } as Subset-Family of PM ;
BALL c= Family_open_set PM

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in BALL ; :: thesis:
then ex c being Point of PM st
( x = H₁(c,m) & S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) ;
hence x in Family_open_set PM by PCOMPS_1:33; :: thesis:

end;

then A in the topology of T by A2, A13, PCOMPS_1:36;
hence A is open by PRE_TOPC:def 5; :: thesis:

end;

A14: Mn well_orders FX by A5, A6, PCOMPS_2:5;
thus Union Un' is Cover of T :: thesis:

proof

[#] T c= union (Union Un')

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A15: x in [#] T ; :: thesis:
defpred S₃[ set ] means x in $1;
ex G being Subset of T st
( x in G & G in FX ) by A3, A15, PCOMPS_1:5;
then A16: ex G being set st
( G in FX & S₃[G] ) ;
consider X being set such that
A17: ( X in FX & S₃[X] & ( for Y being set st Y in FX & S₃[Y] holds
[X,Y] in Mn ) ) from PCOMPS_2:sch 1(A14, A16);
reconsider X = X as Subset of T by A17;
X is open by A4, A17, TOPS_2:def 1;
then A18: X in Family_open_set PM by A2, PRE_TOPC:def 5;
reconsider X = X as Subset of PM by A1, PCOMPS_2:8;
reconsider x' = x as Element of PM by A1, A15, PCOMPS_2:8;
consider r being Real such that
A19: ( r > 0 & Ball x',r c= X ) by A17, A18, PCOMPS_1:def 5;
defpred S₄[ Nat] means 3 / (2 |^ $1) <= r;
ex k being Element of NAT st S₄[k] by A19, PREPOWER:106;
then A20: ex k being Nat st S₄[k] ;
consider k being Nat such that
A21: ( S₄[k] & ( for i being Nat st S₄[i] holds
k <= i ) ) from NAT_1:sch 5(A20);
A22: ( 2 |^ (k + 1) = (2 |^ k) * 2 & 2 |^ k > 0 ) by NEWTON:11, PREPOWER:13;
then 2 |^ (k + 1) >= 2 |^ k by XREAL_1:153;
then 3 / (2 |^ (k + 1)) <= 3 / (2 |^ k) by A22, XREAL_1:120;
then A23: 3 / (2 |^ (k + 1)) <= r by A21, XXREAL_0:2;
assume A24: not x in union (Union Un') ; :: thesis:
A25: for V being set
for n being Element of NAT st V in Un' . n holds
not x in V

proof

let V be set ; :: thesis:
let n be Element of NAT ; :: thesis:
assume V in Un' . n ; :: thesis:
then V in Union Un by PROB_1:25;
hence not x in V by A24, TARSKI:def 4; :: thesis:

end;

A26: for n being Element of NAT holds not x in union (Un' . n)

proof

let n be Element of NAT ; :: thesis:
assume x in union (Un' . n) ; :: thesis:
then consider V being set such that
A27: ( x in V & V in Un' . n ) by TARSKI:def 4;
thus contradiction by A25, A27; :: thesis:

end;

set W = union { H₁(y,k) where y is Point of PM : ( S₁[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) } ;
A28: x in union { H₁(y,k) where y is Point of PM : ( S₁[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) }

proof

set A = Ball x',(1 / (2 |^ (k + 1)));
0 < 2 |^ (k + 1) by PREPOWER:13;
then 0 < 1 / (2 |^ (k + 1)) by XREAL_1:141;
then A29: x' in Ball x',(1 / (2 |^ (k + 1))) by TBSP_1:16;
not x' in PartUnion X,Mn

proof

assume x' in PartUnion X,Mn ; :: thesis:
then x' in union (Mn -Seg X) by PCOMPS_2:def 1;
then consider M being set such that
A30: ( x' in M & M in Mn -Seg X ) by TARSKI:def 4;
A31: ( M <> X & [M,X] in Mn ) by A30, WELLORD1:def 1;
then M in field Mn by RELAT_1:30;
then A32: M in FX by A5, A6, PCOMPS_2:5;
then ( [X,M] in Mn & Mn is_antisymmetric_in FX ) by A14, A17, A30, WELLORD1:def 5;
hence contradiction by A17, A31, A32, RELAT_2:def 4; :: thesis:

end;

then A33: x' in X \ (PartUnion X,Mn) by A17, XBOOLE_0:def 5;
Ball x',(3 / (2 |^ (k + 1))) c= Ball x',r by A23, PCOMPS_1:1;
then A34: Ball x',(3 / (2 |^ (k + 1))) c= X by A19, XBOOLE_1:1;
not x' in union { (union (Un' . i)) where i is Element of NAT : i <= k }

proof

assume x' in union { (union (Un' . i)) where i is Element of NAT : i <= k } ; :: thesis:
then consider D being set such that
A35: ( x' in D & D in { (union (Un' . i)) where i is Element of NAT : i <= k } ) by TARSKI:def 4;
consider i being Element of NAT such that
A36: ( D = union (Un' . i) & i <= k ) by A35;
thus contradiction by A26, A35, A36; :: thesis:

end;

then Ball x',(1 / (2 |^ (k + 1))) in { H₁(y,k) where y is Point of PM : ( S₁[y,X,k] & not y in union { (union (Un' . i)) where i is Element of NAT : i <= k } ) } by A33, A34;
hence x in union { H₁(y,k) where y is Point of PM : ( S₁[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) } by A29, TARSKI:def 4; :: thesis:

end;

A37: k in NAT by ORDINAL1:def 13;
union { H₁(y,k) where y is Point of PM : ( S₁[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) } in { (union { H₁(y,k) where y is Point of PM : ( S₁[y,V,k] & not y in union { (union (Un . q)) where q is Element of NAT : q <= k } ) } ) where V is Subset of PM : V in FX } by A17;
then union { H₁(y,k) where y is Point of PM : ( S₁[y,X,k] & not y in union { (union (Un . i)) where i is Element of NAT : i <= k } ) } in Un' . (k + 1) by A9, A37;
hence contradiction by A25, A28; :: thesis:

end;

then [#] T = union (Union Un') by XBOOLE_0:def 10;
hence Union Un' is Cover of T by SETFAM_1:60; :: thesis:

end;

thus Union Un' is_finer_than FX :: thesis:

proof

for X being set st X in Union Un' holds
ex Y being set st
( Y in FX & X c= Y )

proof

let X be set ; :: thesis:
assume X in Union Un' ; :: thesis:
then consider n being Element of NAT such that
A38: X in Un . n by PROB_1:25;

per cases ;

suppose n = 0 ; :: thesis:

then consider V being Subset of PM such that
A39: ( X = union { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } & V in FX ) by A9, A38;
set BALL = { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ;
{ (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } c= bool the carrier of PM

proof

end;

then reconsider BALL = { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } as Subset-Family of PM ;
for W being set st W in BALL holds
W c= V

proof

let W be set ; :: thesis:
assume W in BALL ; :: thesis:
then consider c being Element of PM such that
A40: ( W = Ball c,(1 / 2) & c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) ;
Ball c,(1 / 2) c= Ball c,(3 / 2) by PCOMPS_1:1;
hence W c= V by A40, XBOOLE_1:1; :: thesis:

end;

then ( X c= V & V in FX ) by A39, ZFMISC_1:94;
hence ex Y being set st
( Y in FX & X c= Y ) ; :: thesis:

end;

suppose n > 0 ; :: thesis:

then consider m being Nat such that
A41: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
X in { (union { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) where V is Subset of PM : S₂[V] } by A9, A38, A41;
then consider V being Subset of PM such that
A42: ( X = union { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } & S₂[V] ) ;
set BALL = { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ;
{ H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } c= bool the carrier of PM

proof

end;

then reconsider BALL = { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } as Subset-Family of PM ;
for W being set st W in BALL holds
W c= V

proof

let W be set ; :: thesis:
assume W in BALL ; :: thesis:
then consider c being Element of PM such that
A43: ( W = H₁(c,m) & S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) ;
0 < 2 |^ (m + 1) by PREPOWER:13;
then 1 / (2 |^ (m + 1)) < 3 / (2 |^ (m + 1)) by XREAL_1:76;
then H₁(c,m) c= Ball c,(3 / (2 |^ (m + 1))) by PCOMPS_1:1;
hence W c= V by A43, XBOOLE_1:1; :: thesis:

end;

then ( X c= V & V in FX ) by A42, ZFMISC_1:94;
hence ex Y being set st
( Y in FX & X c= Y ) ; :: thesis:

end;

hence Union Un' is_finer_than FX by SETFAM_1:def 2; :: thesis:

end;

thus Un' is sigma_discrete :: thesis:

proof

for n being Element of NAT holds Un' . n is discrete

proof

let n be Element of NAT ; :: thesis:
for p being Point of T ex O being open Subset of T st
( p in O & ( for A, B being Subset of T st A in Un' . n & B in Un' . n & O meets A & O meets B holds
A = B ) )

proof

let p be Point of T; :: thesis:
reconsider p' = p as Point of PM by A1, PCOMPS_2:8;
set O = Ball p',(1 / (2 |^ (n + 2)));
0 < 2 |^ (n + 2) by PREPOWER:13;
then A44: 0 < 1 / (2 |^ (n + 2)) by XREAL_1:141;
then ( p' in Ball p',(1 / (2 |^ (n + 2))) & Ball p',(1 / (2 |^ (n + 2))) in Family_open_set PM ) by PCOMPS_1:33, TBSP_1:16;
then reconsider O = Ball p',(1 / (2 |^ (n + 2))) as open Subset of T by A2, PRE_TOPC:def 5;
take O ; :: thesis:

now

let A, B be Subset of T; :: thesis:
assume A45: ( A in Un' . n & B in Un' . n ) ; :: thesis:
assume A46: ( O meets A & O meets B ) ; :: thesis:
then consider a being set such that
A47: ( a in O & a in A ) by XBOOLE_0:3;
consider b being set such that
A48: ( b in O & b in B ) by A46, XBOOLE_0:3;
reconsider a = a, b = b as Point of PM by A47, A48;
( dist p',a < 1 / (2 |^ (n + 2)) & dist p',b < 1 / (2 |^ (n + 2)) & dist p',a = dist a,p' ) by A47, A48, METRIC_1:12;
then ( (dist a,p') + (dist p',b) < (1 / (2 |^ (n + 2))) + (1 / (2 |^ (n + 2))) & dist a,b <= (dist a,p') + (dist p',b) ) by METRIC_1:4, XREAL_1:10;
then ( dist a,b < (1 / (2 |^ (n + 2))) + (1 / (2 |^ (n + 2))) & 2 |^ ((n + 1) + 1) = (2 |^ (n + 1)) * 2 ) by NEWTON:11, XXREAL_0:2;
then dist a,b < 2 * (1 / (2 * (2 |^ (n + 1)))) ;
then dist a,b < (2 * 1) / (2 * (2 |^ (n + 1))) by XCMPLX_1:75;
then A49: dist a,b < ((2 / 2) * 1) / (2 |^ (n + 1)) by XCMPLX_1:84;

now

per cases ;

suppose A50: n = 0 ; :: thesis:

then consider V being Subset of PM such that
A51: ( A = union { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } & V in FX ) by A9, A45;
consider Ba being set such that
A52: ( a in Ba & Ba in { (Ball c,(1 / 2)) where c is Point of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ) by A47, A51, TARSKI:def 4;
consider ca being Point of PM such that
A53: ( Ba = Ball ca,(1 / 2) & ca in V \ (PartUnion V,Mn) & Ball ca,(3 / 2) c= V ) by A52;
consider W being Subset of PM such that
A54: ( B = union { (Ball c,(1 / 2)) where c is Point of PM : ( c in W \ (PartUnion W,Mn) & Ball c,(3 / 2) c= W ) } & W in FX ) by A9, A45, A50;
consider Bb being set such that
A55: ( b in Bb & Bb in { (Ball c,(1 / 2)) where c is Point of PM : ( c in W \ (PartUnion W,Mn) & Ball c,(3 / 2) c= W ) } ) by A48, A54, TARSKI:def 4;
consider cb being Point of PM such that
A56: ( Bb = Ball cb,(1 / 2) & cb in W \ (PartUnion W,Mn) & Ball cb,(3 / 2) c= W ) by A55;
( dist ca,a < 1 / 2 & dist a,b < 1 / 2 ) by A49, A50, A52, A53, METRIC_1:12, NEWTON:10;
then ( (dist ca,a) + (dist a,b) < (1 / 2) + (1 / 2) & dist ca,b <= (dist ca,a) + (dist a,b) ) by METRIC_1:4, XREAL_1:10;
then ( dist ca,b < 1 & dist cb,b < 1 / 2 & dist cb,b = dist b,cb ) by A55, A56, METRIC_1:12, XXREAL_0:2;
then ( (dist ca,b) + (dist b,cb) < 1 + (1 / 2) & dist ca,cb <= (dist ca,b) + (dist b,cb) ) by METRIC_1:4, XREAL_1:10;
then ( dist ca,cb < 3 / 2 & dist ca,cb = dist cb,ca ) by XXREAL_0:2;
then A57: ( ca in Ball cb,(3 / 2) & cb in Ball ca,(3 / 2) ) by METRIC_1:12;
V = W

proof

assume A58: V <> W ; :: thesis:
Mn is_connected_in FX by A14, WELLORD1:def 5;
then ( [V,W] in Mn or [W,V] in Mn ) by A51, A54, A58, RELAT_2:def 6;
then ( V in Mn -Seg W or W in Mn -Seg V ) by A58, WELLORD1:def 1;
then ( cb in union (Mn -Seg W) or ca in union (Mn -Seg V) ) by A53, A56, A57, TARSKI:def 4;
then ( cb in PartUnion W,Mn or ca in PartUnion V,Mn ) by PCOMPS_2:def 1;
hence contradiction by A53, A56, XBOOLE_0:def 5; :: thesis:

end;

hence A = B by A51, A54; :: thesis:

end;

suppose n > 0 ; :: thesis:

then consider m being Nat such that
A59: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A in { (union { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) where V is Subset of PM : S₂[V] } by A9, A45, A59;
then consider V being Subset of PM such that
A60: ( A = union { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } & S₂[V] ) ;
consider Ba being set such that
A61: ( a in Ba & Ba in { H₁(c,m) where c is Point of PM : ( S₁[c,V,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) by A47, A60, TARSKI:def 4;
consider ca being Point of PM such that
A62: ( Ba = H₁(ca,m) & S₁[ca,V,m] & not ca in union { (union (Un . k)) where k is Element of NAT : k <= m } ) by A61;
B in { (union { H₁(c,m) where c is Point of PM : ( S₁[c,W,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) where W is Subset of PM : S₂[W] } by A9, A45, A59;
then consider W being Subset of PM such that
A63: ( B = union { H₁(c,m) where c is Point of PM : ( S₁[c,W,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } & S₂[W] ) ;
consider Bb being set such that
A64: ( b in Bb & Bb in { H₁(c,m) where c is Point of PM : ( S₁[c,W,m] & not c in union { (union (Un . k)) where k is Element of NAT : k <= m } ) } ) by A48, A63, TARSKI:def 4;
consider cb being Point of PM such that
A65: ( Bb = H₁(cb,m) & S₁[cb,W,m] & not cb in union { (union (Un . k)) where k is Element of NAT : k <= m } ) by A64;
set r = 1 / (2 |^ n);
A66: ( 2 |^ (n + 1) = (2 |^ n) * 2 & 2 |^ n > 0 ) by NEWTON:11, PREPOWER:13;
then 2 |^ (n + 1) >= 2 |^ n by XREAL_1:153;
then 1 / (2 |^ (n + 1)) <= 1 / (2 |^ n) by A66, XREAL_1:120;
then ( dist ca,a < 1 / (2 |^ n) & dist a,b < 1 / (2 |^ n) ) by A49, A59, A61, A62, METRIC_1:12, XXREAL_0:2;
then ( (dist ca,a) + (dist a,b) < (1 / (2 |^ n)) + (1 / (2 |^ n)) & dist ca,b <= (dist ca,a) + (dist a,b) ) by METRIC_1:4, XREAL_1:10;
then ( dist ca,b < (1 / (2 |^ n)) + (1 / (2 |^ n)) & dist cb,b < 1 / (2 |^ n) & dist cb,b = dist b,cb ) by A59, A64, A65, METRIC_1:12, XXREAL_0:2;
then ( (dist ca,b) + (dist b,cb) < ((1 / (2 |^ n)) + (1 / (2 |^ n))) + (1 / (2 |^ n)) & dist ca,cb <= (dist ca,b) + (dist b,cb) ) by METRIC_1:4, XREAL_1:10;
then ( dist ca,cb < 3 * (1 / (2 |^ n)) & dist ca,cb = dist cb,ca & 3 * (1 / (2 |^ n)) = (3 * 1) / (2 |^ n) ) by XCMPLX_1:75, XXREAL_0:2;
then A67: ( ca in Ball cb,(3 / (2 |^ (m + 1))) & cb in Ball ca,(3 / (2 |^ (m + 1))) ) by A59, METRIC_1:12;
V = W

proof

assume A68: V <> W ; :: thesis:
Mn is_connected_in FX by A14, WELLORD1:def 5;
then ( [V,W] in Mn or [W,V] in Mn ) by A60, A63, A68, RELAT_2:def 6;
then ( V in Mn -Seg W or W in Mn -Seg V ) by A68, WELLORD1:def 1;
then ( cb in union (Mn -Seg W) or ca in union (Mn -Seg V) ) by A62, A65, A67, TARSKI:def 4;
then ( cb in PartUnion W,Mn or ca in PartUnion V,Mn ) by PCOMPS_2:def 1;
hence contradiction by A62, A65, XBOOLE_0:def 5; :: thesis:

end;

hence A = B by A60, A63; :: thesis:

end;

hence A = B ; :: thesis:

end;

hence ( p in O & ( for A, B being Subset of T st A in Un' . n & B in Un' . n & O meets A & O meets B holds
A = B ) ) by A44, TBSP_1:16; :: thesis:

end;

hence Un' . n is discrete by NAGATA_1:def 1; :: thesis:

end;

hence Un' is sigma_discrete by NAGATA_1:def 2; :: thesis:

end;