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_{1}[ set ] means $1 in FX;

deffunc H_{1}( 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

defpred S_{2}[ 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_{1}(c,n) where c is Point of PM : ( S_{2}[c,V,n] & not c in union { (union (Un . k)) where k is Nat : k <= n } ) } ) where V is Subset of PM : S_{1}[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 )

[#] T c= 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 )

for n being Element of NAT holds Un9 . n is discrete

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

deffunc H

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

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 ;
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

end;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

hence
x in bool the carrier of PM
; :: thesis: verum
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;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

defpred S

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

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

A15:
Mn well_orders FX
by A5, A6, PCOMPS_2:1;
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;

end;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 )
;

end;

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

BALL c= Family_open_set PM

hence A is open by PRE_TOPC:def 2; :: thesis: verum

end;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

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 ;
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;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

BALL c= Family_open_set PM

proof

then
A in the topology of T
by A2, A12, PCOMPS_1:32;
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;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

hence A is open by PRE_TOPC:def 2; :: thesis: verum

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_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } ) where V is Subset of PM : S_{1}[V] }
by A10, A11, A13;

then consider V being Subset of PM such that

A14: ( A = union { H_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } & S_{1}[V] )
;

set BALL = { H_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } ;

{ H_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } c= bool the carrier of PM
_{1}(c,m) where c is Point of PM : ( S_{2}[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

hence A is open by PRE_TOPC:def 2; :: thesis: verum

end;A13: n = m + 1 by NAT_1:6;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

A in { (union { H

then consider V being Subset of PM such that

A14: ( A = union { H

set BALL = { H

{ H

proof

then reconsider BALL = { H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H_{1}(c,m) where c is Point of PM : ( S_{2}[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_{1}(c,m) where c is Point of PM : ( S_{2}[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_{1}(c,m) & S_{2}[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;assume x in { H

then ex c being Point of PM st

( x = H

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

BALL c= Family_open_set PM

proof

then
A in the topology of T
by A2, A14, PCOMPS_1:32;
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_{1}(c,m) & S_{2}[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;assume x in BALL ; :: thesis: x in Family_open_set PM

then ex c being Point of PM st

( x = H

hence x in Family_open_set PM by PCOMPS_1:29; :: thesis: verum

hence A is open by PRE_TOPC:def 2; :: thesis: verum

[#] T c= union (Union Un9)

proof

then
[#] T = union (Union Un9)
;
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_{3}[ 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_{3}[G] )
;

consider X being set such that

A18: ( X in FX & S_{3}[X] & ( for Y being set st Y in FX & S_{3}[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

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_{4}[ Nat] means 3 / (2 |^ $1) <= r;

ex k being Nat st S_{4}[k]
by A23, PREPOWER:92;

then A25: ex k being Nat st S_{4}[k]
;

consider k being Nat such that

A26: ( S_{4}[k] & ( for i being Nat st S_{4}[i] holds

k <= i ) ) from NAT_1:sch 5(A25);

set W = union { H_{1}(y,k) where y is Point of PM : ( S_{2}[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_{1}(y,k) where y is Point of PM : ( S_{2}[y,X,k] & not y in union { (union (Un . i)) where i is Nat : i <= k } ) }
_{1}(y,k) where y is Point of PM : ( S_{2}[y,X,k] & not y in union { (union (Un . i)) where i is Nat : i <= k } ) } in { (union { H_{1}(y,k) where y is Point of PM : ( S_{2}[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_{1}(y,k) where y is Point of PM : ( S_{2}[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;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

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

consider X being set such that

A18: ( X in FX & S

[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

A21:
for n being Nat holds not x in union (Un9 . n)
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;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

proof

reconsider X = X as Subset of T by A18;
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;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

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

ex k being Nat st S

then A25: ex k being Nat st S

consider k being Nat such that

A26: ( S

k <= i ) ) from NAT_1:sch 5(A25);

set W = union { H

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

proof

( k in NAT & union { H
not x9 in PartUnion (X,Mn)

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 }

then Ball (x9,(3 / (2 |^ (k + 1)))) c= X by A24;

then Ball (x9,(1 / (2 |^ (k + 1)))) in { H_{1}(y,k) where y is Point of PM : ( S_{2}[y,X,k] & not y in union { (union (Un9 . i)) where i is Nat : i <= k } ) }
by A35, A37;

hence x in union { H_{1}(y,k) where y is Point of PM : ( S_{2}[y,X,k] & not y in union { (union (Un . i)) where i is Nat : i <= k } ) }
by A36, TARSKI:def 4; :: thesis: verum

end;proof

then A35:
x9 in X \ (PartUnion (X,Mn))
by A18, XBOOLE_0:def 5;
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 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

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

Ball (x9,(3 / (2 |^ (k + 1)))) c= Ball (x9,r)
by A27, PCOMPS_1:1;
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;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

then Ball (x9,(3 / (2 |^ (k + 1)))) c= X by A24;

then Ball (x9,(1 / (2 |^ (k + 1)))) in { H

hence x in union { H

then union { H

hence contradiction by A20, A28; :: thesis: verum

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

hence
Union Un9 is_finer_than FX
by SETFAM_1:def 2; :: thesis: Un9 is sigma_discrete
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;

end;( 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 )
;

end;

suppose
n = 0
; :: thesis: ex Y being set st

( Y in FX & X c= Y )

( 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

for W being set st W in BALL holds

W c= V

hence ex Y being set st

( Y in FX & X c= Y ) by A41; :: thesis: verum

end;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

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 ;
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;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

for W being set st W in BALL holds

W c= V

proof

then
X c= V
by A40, ZFMISC_1:76;
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;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

hence ex Y being set st

( Y in FX & X c= Y ) by A41; :: thesis: verum

suppose
n > 0
; :: thesis: ex Y being set st

( Y in FX & X c= Y )

( 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_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } ) where V is Subset of PM : S_{1}[V] }
by A10, A39, A44;

then consider V being Subset of PM such that

A45: ( X = union { H_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } & S_{1}[V] )
;

set BALL = { H_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } ;

{ H_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } c= bool the carrier of PM
_{1}(c,m) where c is Point of PM : ( S_{2}[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

hence ex Y being set st

( Y in FX & X c= Y ) by A45; :: thesis: verum

end;A44: n = m + 1 by NAT_1:6;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

X in { (union { H

then consider V being Subset of PM such that

A45: ( X = union { H

set BALL = { H

{ H

proof

then reconsider BALL = { H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H_{1}(c,m) where c is Point of PM : ( S_{2}[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_{1}(c,m) where c is Point of PM : ( S_{2}[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_{1}(c,m) & S_{2}[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;assume x in { H

then ex c being Point of PM st

( x = H

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

for W being set st W in BALL holds

W c= V

proof

then
X c= V
by A45, ZFMISC_1:76;
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_{1}(c,m) & S_{2}[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_{1}(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;assume W in BALL ; :: thesis: W c= V

then consider c being Element of PM such that

A46: ( W = H

0 < 2 |^ (m + 1) by PREPOWER:6;

then 1 / (2 |^ (m + 1)) < 3 / (2 |^ (m + 1)) by XREAL_1:74;

then H

hence W c= V by A46, XBOOLE_1:1; :: thesis: verum

hence ex Y being set st

( Y in FX & X c= Y ) by A45; :: thesis: verum

for n being Element of NAT holds Un9 . n is discrete

proof

hence
Un9 is sigma_discrete
by NAGATA_1:def 2; :: thesis: verum
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 ) )

end;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

hence
Un9 . n is discrete
by NAGATA_1:def 1; :: thesis: verum
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 ) )

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;( 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

0 < 2 |^ (n + 2)
by PREPOWER:6;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;

end;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 = Bend;

hence
A = B
; :: thesis: verumper cases
( n = 0 or n > 0 )
;

end;

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

end;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

hence
A = B
by A61, A70; :: thesis: verum
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;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

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_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } ) where V is Subset of PM : S_{1}[V] }
by A10, A48, A80;

then consider V being Subset of PM such that

A83: ( A = union { H_{1}(c,m) where c is Point of PM : ( S_{2}[c,V,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } & S_{1}[V] )
;

consider Ba being set such that

A84: ( a in Ba & Ba in { H_{1}(c,m) where c is Point of PM : ( S_{2}[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_{1}(ca,m) & S_{2}[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_{1}(c,m) where c is Point of PM : ( S_{2}[c,W,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } ) where W is Subset of PM : S_{1}[W] }
by A10, A49, A80;

then consider W being Subset of PM such that

A88: ( B = union { H_{1}(c,m) where c is Point of PM : ( S_{2}[c,W,m] & not c in union { (union (Un . k)) where k is Nat : k <= m } ) } & S_{1}[W] )
;

consider Bb being set such that

A89: ( b in Bb & Bb in { H_{1}(c,m) where c is Point of PM : ( S_{2}[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_{1}(cb,m) & S_{2}[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

end;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

then consider V being Subset of PM such that

A83: ( A = union { H

consider Ba being set such that

A84: ( a in Ba & Ba in { H

consider ca being Point of PM such that

A85: ( Ba = H

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

then consider W being Subset of PM such that

A88: ( B = union { H

consider Bb being set such that

A89: ( b in Bb & Bb in { H

consider cb being Point of PM such that

A90: ( Bb = H

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

hence
A = B
by A83, A88; :: thesis: verum
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;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

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