let T be non empty TopSpace; :: thesis: ( T is metrizable implies for FX being Subset-Family of T st FX is Cover of T & FX is open holds
ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete ) )
set cT = the carrier of T;
assume T is metrizable ; :: thesis: for FX being Subset-Family of T st FX is Cover of T & FX is open holds
ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete )
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 8;
reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A1, PCOMPS_1:36;
set cPM = the carrier of PM;
let FX be Subset-Family of T; :: thesis: ( FX is Cover of T & FX is open implies ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete ) )
assume that
A3: FX is Cover of T and
A4: FX is open ; :: thesis: ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete )
defpred S₁[ set ] means $1 in FX;
deffunc H₁( Point of PM, Nat) -> Element of bool the carrier of PM = Ball ($1,(1 / (2 |^ ($2 + 1))));
consider R being Relation such that
A5: R well_orders FX by WELLORD2:17;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not 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 } or x in bool the carrier of PM )
reconsider xx = x as set by TARSKI:1;
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: x in bool the carrier of PM
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 ;
xx c= the carrier of PM

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in xx or y in the carrier of PM )
assume y in xx ; :: thesis: y in the carrier of PM
then consider W being set such that
A8: y in W and
A9: 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 A9;
hence y in the carrier of PM by A8; :: thesis: verum

end;

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

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 ;
defpred S₂[ Point of PM, Subset of PM, Nat] means ( $1 in $2 \ (PartUnion ($2,Mn)) & Ball ($1,(3 / (2 |^ ($3 + 1)))) c= $2 );
consider Un being sequence of (bool (bool the carrier of PM)) such that
A10: ( Un . 0 = UB & ( for n being 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 Nat : k <= n } ) } ) where V is Subset of PM : S₁[V] } ) ) from PCOMPS_2:sch 3();
reconsider Un9 = Un as FamilySequence of T by A1, PCOMPS_2:4;
take Un9 ; :: thesis: ( Union Un9 is open & Union Un9 is Cover of T & Union Un9 is_finer_than FX & Un9 is sigma_discrete )
thus Union Un9 is open :: thesis: ( Union Un9 is Cover of T & Union Un9 is_finer_than FX & Un9 is sigma_discrete )

proof

let A be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not A in Union Un9 or A is open )
assume A in Union Un9 ; :: thesis: A is open
then consider n being Nat such that
A11: A in Un . n by PROB_1:12;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: A is open

then consider V being Subset of PM such that
A12: 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 A10, A11;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } or x in bool the carrier of PM )
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: x in bool the carrier of PM
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: verum

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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in BALL or x in Family_open_set PM )
assume x in BALL ; :: thesis: x in Family_open_set PM
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:29; :: thesis: verum

end;

then A in the topology of T by A2, A12, PCOMPS_1:32;
hence A is open by PRE_TOPC:def 2; :: thesis: verum

end;

suppose n > 0 ; :: thesis: A is open

then consider m being Nat such that
A13: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
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 Nat : k <= m } ) } ) where V is Subset of PM : S₁[V] } by A10, A11, A13;
then consider V being Subset of PM such that
A14: ( 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 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 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 Nat : k <= m } ) } c= bool the carrier of PM

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 Nat : k <= m } ) } or x in bool the carrier of PM )
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 Nat : k <= m } ) } ; :: thesis: x in bool the carrier of PM
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 Nat : k <= m } ) ;
hence x in bool the carrier of PM ; :: thesis: verum

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 Nat : k <= m } ) } as Subset-Family of PM ;
BALL c= Family_open_set PM

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in BALL or x in Family_open_set PM )
assume x in BALL ; :: thesis: x in Family_open_set PM
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 Nat : k <= m } ) ;
hence x in Family_open_set PM by PCOMPS_1:29; :: thesis: verum

end;

then A in the topology of T by A2, A14, PCOMPS_1:32;
hence A is open by PRE_TOPC:def 2; :: thesis: verum

end;

end;

end;

A15: Mn well_orders FX by A5, A6, PCOMPS_2:1;
[#] T c= union (Union Un9)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] T or x in union (Union Un9) )
assume A16: x in [#] T ; :: thesis: x in union (Union Un9)
reconsider x9 = x as Element of PM by A1, A16, PCOMPS_2:4;
defpred S₃[ set ] means x in $1;
ex G being Subset of T st
( x in G & G in FX ) by A3, A16, PCOMPS_1:3;
then A17: ex G being set st
( G in FX & S₃[G] ) ;
consider X being set such that
A18: ( 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(A15, A17);
assume A19: not x in union (Union Un9) ; :: thesis: contradiction
A20: for V being set
for n being Nat st V in Un9 . n holds
not x in V

proof

let V be set ; :: thesis: for n being Nat st V in Un9 . n holds
not x in V
let n be Nat; :: thesis: ( V in Un9 . n implies not x in V )
assume V in Un9 . n ; :: thesis: not x in V
then V in Union Un by PROB_1:12;
hence not x in V by A19, TARSKI:def 4; :: thesis: verum

end;

A21: for n being Nat holds not x in union (Un9 . n)

proof

let n be Nat; :: thesis: not x in union (Un9 . n)
assume x in union (Un9 . n) ; :: thesis: contradiction
then ex V being set st
( x in V & V in Un9 . n ) by TARSKI:def 4;
hence contradiction by A20; :: thesis: verum

end;

reconsider X = X as Subset of T by A18;
X is open by A4, A18;
then A22: X in Family_open_set PM by A2, PRE_TOPC:def 2;
reconsider X = X as Subset of PM by A1, PCOMPS_2:4;
consider r being Real such that
A23: r > 0 and
A24: Ball (x9,r) c= X by A18, A22, PCOMPS_1:def 4;
defpred S₄[ Nat] means 3 / (2 |^ $1) <= r;
ex k being Nat st S₄[k] by A23, PREPOWER:92;
then A25: ex k being Nat st S₄[k] ;
consider k being Nat such that
A26: ( S₄[k] & ( for i being Nat st S₄[i] holds
k <= i ) ) from NAT_1:sch 5(A25);
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 Nat : i <= k } ) } ;
2 |^ (k + 1) = (2 |^ k) * 2 by NEWTON:6;
then ( 2 |^ k > 0 & 2 |^ (k + 1) >= 2 |^ k ) by PREPOWER:6, XREAL_1:151;
then 3 / (2 |^ (k + 1)) <= 3 / (2 |^ k) by XREAL_1:118;
then A27: 3 / (2 |^ (k + 1)) <= r by A26, XXREAL_0:2;
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 Nat : i <= k } ) }

proof

not x9 in PartUnion (X,Mn)

proof

assume x9 in PartUnion (X,Mn) ; :: thesis: contradiction
then x9 in union (Mn -Seg X) by PCOMPS_2:def 1;
then consider M being set such that
A29: x9 in M and
A30: M in Mn -Seg X by TARSKI:def 4;
A31: M <> X by A30, WELLORD1:1;
A32: Mn is_antisymmetric_in FX by A15, WELLORD1:def 5;
A33: [M,X] in Mn by A30, WELLORD1:1;
then M in field Mn by RELAT_1:15;
then A34: M in FX by A5, A6, PCOMPS_2:1;
then [X,M] in Mn by A18, A29;
hence contradiction by A18, A31, A33, A34, A32, RELAT_2:def 4; :: thesis: verum

end;

then A35: x9 in X \ (PartUnion (X,Mn)) by A18, XBOOLE_0:def 5;
set A = Ball (x9,(1 / (2 |^ (k + 1))));
0 < 2 |^ (k + 1) by PREPOWER:6;
then A36: x9 in Ball (x9,(1 / (2 |^ (k + 1)))) by TBSP_1:11, XREAL_1:139;
A37: not x9 in union { (union (Un9 . i)) where i is Nat : i <= k }

proof

assume x9 in union { (union (Un9 . i)) where i is Nat : i <= k } ; :: thesis: contradiction
then consider D being set such that
A38: ( x9 in D & D in { (union (Un9 . i)) where i is Nat : i <= k } ) by TARSKI:def 4;
ex i being Nat st
( D = union (Un9 . i) & i <= k ) by A38;
hence contradiction by A21, A38; :: thesis: verum

end;

Ball (x9,(3 / (2 |^ (k + 1)))) c= Ball (x9,r) by A27, PCOMPS_1:1;
then Ball (x9,(3 / (2 |^ (k + 1)))) c= X by A24;
then Ball (x9,(1 / (2 |^ (k + 1)))) in { H₁(y,k) where y is Point of PM : ( S₂[y,X,k] & not y in union { (union (Un9 . i)) where i is Nat : i <= k } ) } by A35, A37;
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 Nat : i <= k } ) } by A36, TARSKI:def 4; :: thesis: verum

end;

( k in NAT & union { H₁(y,k) where y is Point of PM : ( S₂[y,X,k] & not y in union { (union (Un . i)) where i is 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 Nat : q <= k } ) } ) where V is Subset of PM : V in FX } ) by A18, ORDINAL1:def 12;
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 Nat : i <= k } ) } in Un9 . (k + 1) by A10;
hence contradiction by A20, A28; :: thesis: verum

end;

then [#] T = union (Union Un9) ;
hence Union Un9 is Cover of T by SETFAM_1:45; :: thesis: ( Union Un9 is_finer_than FX & Un9 is sigma_discrete )
for X being set st X in Union Un9 holds
ex Y being set st
( Y in FX & X c= Y )

proof

let X be set ; :: thesis: ( X in Union Un9 implies ex Y being set st
( Y in FX & X c= Y ) )
assume X in Union Un9 ; :: thesis: ex Y being set st
( Y in FX & X c= Y )
then consider n being Nat such that
A39: X in Un . n by PROB_1:12;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: ex Y being set st
( Y in FX & X c= Y )

then consider V being Subset of PM such that
A40: 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
A41: V in FX by A10, A39;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Ball (c,(1 / 2))) where c is Point of PM : ( c in V \ (PartUnion (V,Mn)) & Ball (c,(3 / 2)) c= V ) } or x in bool the carrier of PM )
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: x in bool the carrier of PM
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: verum

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: ( W in BALL implies W c= V )
assume W in BALL ; :: thesis: W c= V
then consider c being Element of PM such that
A42: W = Ball (c,(1 / 2)) and
c in V \ (PartUnion (V,Mn)) and
A43: Ball (c,(3 / 2)) c= V ;
Ball (c,(1 / 2)) c= Ball (c,(3 / 2)) by PCOMPS_1:1;
hence W c= V by A42, A43; :: thesis: verum

end;

then X c= V by A40, ZFMISC_1:76;
hence ex Y being set st
( Y in FX & X c= Y ) by A41; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex Y being set st
( Y in FX & X c= Y )

then consider m being Nat such that
A44: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
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 Nat : k <= m } ) } ) where V is Subset of PM : S₁[V] } by A10, A39, A44;
then consider V being Subset of PM such that
A45: ( 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 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 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 Nat : k <= m } ) } c= bool the carrier of PM

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not 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 Nat : k <= m } ) } or x in bool the carrier of PM )
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 Nat : k <= m } ) } ; :: thesis: x in bool the carrier of PM
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 Nat : k <= m } ) ;
hence x in bool the carrier of PM ; :: thesis: verum

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 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: ( W in BALL implies W c= V )
assume W in BALL ; :: thesis: W c= V
then consider c being Element of PM such that
A46: ( W = H₁(c,m) & S₂[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) ;
0 < 2 |^ (m + 1) by PREPOWER:6;
then 1 / (2 |^ (m + 1)) < 3 / (2 |^ (m + 1)) by XREAL_1:74;
then H₁(c,m) c= Ball (c,(3 / (2 |^ (m + 1)))) by PCOMPS_1:1;
hence W c= V by A46, XBOOLE_1:1; :: thesis: verum

end;

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

end;

end;

end;

hence Union Un9 is_finer_than FX by SETFAM_1:def 2; :: thesis: Un9 is sigma_discrete
for n being Element of NAT holds Un9 . n is discrete

proof

let n be Element of NAT ; :: thesis: Un9 . n is discrete
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 Un9 . n & B in Un9 . n & O meets A & O meets B holds
A = B ) )

proof

let p be Point of T; :: thesis: ex O being open Subset of T st
( p in O & ( for A, B being Subset of T st A in Un9 . n & B in Un9 . n & O meets A & O meets B holds
A = B ) )
reconsider p9 = p as Point of PM by A1, PCOMPS_2:4;
set O = Ball (p9,(1 / (2 |^ (n + 2))));
Ball (p9,(1 / (2 |^ (n + 2)))) in Family_open_set PM by PCOMPS_1:29;
then reconsider O = Ball (p9,(1 / (2 |^ (n + 2)))) as open Subset of T by A2, PRE_TOPC:def 2;
take O ; :: thesis: ( p in O & ( for A, B being Subset of T st A in Un9 . n & B in Un9 . n & O meets A & O meets B holds
A = B ) )

A47: now :: thesis: for A, B being Subset of T st A in Un9 . n & B in Un9 . n & O meets A & O meets B holds
A = B

let A, B be Subset of T; :: thesis: ( A in Un9 . n & B in Un9 . n & O meets A & O meets B implies A = B )
assume that
A48: A in Un9 . n and
A49: B in Un9 . n ; :: thesis: ( O meets A & O meets B implies A = B )
assume that
A50: O meets A and
A51: O meets B ; :: thesis: A = B
consider a being object such that
A52: a in O and
A53: a in A by A50, XBOOLE_0:3;
consider b being object such that
A54: b in O and
A55: b in B by A51, XBOOLE_0:3;
reconsider a = a, b = b as Point of PM by A52, A54;
A56: dist (p9,b) < 1 / (2 |^ (n + 2)) by A54, METRIC_1:11;
A57: ( dist (a,b) <= (dist (a,p9)) + (dist (p9,b)) & 2 |^ ((n + 1) + 1) = (2 |^ (n + 1)) * 2 ) by METRIC_1:4, NEWTON:6;
dist (p9,a) < 1 / (2 |^ (n + 2)) by A52, METRIC_1:11;
then (dist (a,p9)) + (dist (p9,b)) < (1 / (2 |^ (n + 2))) + (1 / (2 |^ (n + 2))) by A56, XREAL_1:8;
then dist (a,b) < 2 * (1 / (2 * (2 |^ (n + 1)))) by A57, XXREAL_0:2;
then dist (a,b) < (2 * 1) / (2 * (2 |^ (n + 1))) by XCMPLX_1:74;
then A58: dist (a,b) < ((2 / 2) * 1) / (2 |^ (n + 1)) by XCMPLX_1:83;

now :: thesis: A = B

per cases ( n = 0 or n > 0 ) ;

suppose A59: n = 0 ; :: thesis: A = B

then A60: dist (a,b) < 1 / 2 by A58;
consider V being Subset of PM such that
A61: 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
A62: V in FX by A10, A48, A59;
consider Ba being set such that
A63: a in Ba and
A64: 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 A53, A61, TARSKI:def 4;
consider ca being Point of PM such that
A65: Ba = Ball (ca,(1 / 2)) and
A66: ca in V \ (PartUnion (V,Mn)) and
A67: Ball (ca,(3 / 2)) c= V by A64;
dist (ca,a) < 1 / 2 by A63, A65, METRIC_1:11;
then A68: (dist (ca,a)) + (dist (a,b)) < (1 / 2) + (1 / 2) by A60, XREAL_1:8;
dist (ca,b) <= (dist (ca,a)) + (dist (a,b)) by METRIC_1:4;
then A69: dist (ca,b) < 1 by A68, XXREAL_0:2;
consider W being Subset of PM such that
A70: B = union { (Ball (c,(1 / 2))) where c is Point of PM : ( c in W \ (PartUnion (W,Mn)) & Ball (c,(3 / 2)) c= W ) } and
A71: W in FX by A10, A49, A59;
consider Bb being set such that
A72: b in Bb and
A73: 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 A55, A70, TARSKI:def 4;
consider cb being Point of PM such that
A74: Bb = Ball (cb,(1 / 2)) and
A75: cb in W \ (PartUnion (W,Mn)) and
A76: Ball (cb,(3 / 2)) c= W by A73;
A77: dist (ca,cb) <= (dist (ca,b)) + (dist (b,cb)) by METRIC_1:4;
dist (cb,b) < 1 / 2 by A72, A74, METRIC_1:11;
then (dist (ca,b)) + (dist (b,cb)) < 1 + (1 / 2) by A69, XREAL_1:8;
then dist (ca,cb) < 3 / 2 by A77, XXREAL_0:2;
then A78: ( ca in Ball (cb,(3 / 2)) & cb in Ball (ca,(3 / 2)) ) by METRIC_1:11;
V = W

proof

assume A79: V <> W ; :: thesis: contradiction
Mn is_connected_in FX by A15, WELLORD1:def 5;
then ( [V,W] in Mn or [W,V] in Mn ) by A62, A71, A79, RELAT_2:def 6;
then ( V in Mn -Seg W or W in Mn -Seg V ) by A79, WELLORD1:1;
then ( cb in union (Mn -Seg W) or ca in union (Mn -Seg V) ) by A67, A76, A78, TARSKI:def 4;
then ( cb in PartUnion (W,Mn) or ca in PartUnion (V,Mn) ) by PCOMPS_2:def 1;
hence contradiction by A66, A75, XBOOLE_0:def 5; :: thesis: verum

end;

hence A = B by A61, A70; :: thesis: verum

end;

suppose n > 0 ; :: thesis: A = B

then consider m being Nat such that
A80: n = m + 1 by NAT_1:6;
set r = 1 / (2 |^ n);
A81: 3 * (1 / (2 |^ n)) = (3 * 1) / (2 |^ n) by XCMPLX_1:74;
2 |^ (n + 1) = (2 |^ n) * 2 by NEWTON:6;
then ( 2 |^ n > 0 & 2 |^ (n + 1) >= 2 |^ n ) by PREPOWER:6, XREAL_1:151;
then 1 / (2 |^ (n + 1)) <= 1 / (2 |^ n) by XREAL_1:118;
then A82: dist (a,b) < 1 / (2 |^ n) by A58, XXREAL_0:2;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
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 Nat : k <= m } ) } ) where V is Subset of PM : S₁[V] } by A10, A48, A80;
then consider V being Subset of PM such that
A83: ( 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 Nat : k <= m } ) } & S₁[V] ) ;
consider Ba being set such that
A84: ( 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 Nat : k <= m } ) } ) by A53, A83, TARSKI:def 4;
consider ca being Point of PM such that
A85: ( Ba = H₁(ca,m) & S₂[ca,V,m] & not ca in union { (union (Un . k)) where k is Nat : k <= m } ) by A84;
dist (ca,a) < 1 / (2 |^ n) by A80, A84, A85, METRIC_1:11;
then A86: (dist (ca,a)) + (dist (a,b)) < (1 / (2 |^ n)) + (1 / (2 |^ n)) by A82, XREAL_1:8;
dist (ca,b) <= (dist (ca,a)) + (dist (a,b)) by METRIC_1:4;
then A87: dist (ca,b) < (1 / (2 |^ n)) + (1 / (2 |^ n)) by A86, XXREAL_0:2;
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 Nat : k <= m } ) } ) where W is Subset of PM : S₁[W] } by A10, A49, A80;
then consider W being Subset of PM such that
A88: ( 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 Nat : k <= m } ) } & S₁[W] ) ;
consider Bb being set such that
A89: ( 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 Nat : k <= m } ) } ) by A55, A88, TARSKI:def 4;
consider cb being Point of PM such that
A90: ( Bb = H₁(cb,m) & S₂[cb,W,m] & not cb in union { (union (Un . k)) where k is Nat : k <= m } ) by A89;
A91: dist (ca,cb) <= (dist (ca,b)) + (dist (b,cb)) by METRIC_1:4;
dist (cb,b) < 1 / (2 |^ n) by A80, A89, A90, METRIC_1:11;
then (dist (ca,b)) + (dist (b,cb)) < ((1 / (2 |^ n)) + (1 / (2 |^ n))) + (1 / (2 |^ n)) by A87, XREAL_1:8;
then dist (ca,cb) < 3 * (1 / (2 |^ n)) by A91, XXREAL_0:2;
then A92: ( ca in Ball (cb,(3 / (2 |^ (m + 1)))) & cb in Ball (ca,(3 / (2 |^ (m + 1)))) ) by A80, A81, METRIC_1:11;
V = W

proof

assume A93: V <> W ; :: thesis: contradiction
Mn is_connected_in FX by A15, WELLORD1:def 5;
then ( [V,W] in Mn or [W,V] in Mn ) by A83, A88, A93, RELAT_2:def 6;
then ( V in Mn -Seg W or W in Mn -Seg V ) by A93, WELLORD1:1;
then ( cb in union (Mn -Seg W) or ca in union (Mn -Seg V) ) by A85, A90, A92, TARSKI:def 4;
then ( cb in PartUnion (W,Mn) or ca in PartUnion (V,Mn) ) by PCOMPS_2:def 1;
hence contradiction by A85, A90, XBOOLE_0:def 5; :: thesis: verum

end;

hence A = B by A83, A88; :: thesis: verum

end;

end;

end;

hence A = B ; :: thesis: verum

end;

0 < 2 |^ (n + 2) by PREPOWER:6;
hence ( p in O & ( for A, B being Subset of T st A in Un9 . n & B in Un9 . n & O meets A & O meets B holds
A = B ) ) by A47, TBSP_1:11, XREAL_1:139; :: thesis: verum

end;

hence Un9 . n is discrete by NAGATA_1:def 1; :: thesis: verum

end;

hence Un9 is sigma_discrete by NAGATA_1:def 2; :: thesis: verum