let PT be non empty TopSpace; :: thesis: ( PT is metrizable implies for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite ) )
assume PT is metrizable ; :: thesis: for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )
then consider metr being Function of [:the carrier of PT,the carrier of PT:], REAL such that
A1: metr is_metric_of the carrier of PT and
A2: Family_open_set (SpaceMetr the carrier of PT,metr) = the topology of PT by PCOMPS_1:def 9;
consider PM being non empty MetrSpace such that
A3: PM = SpaceMetr the carrier of PT,metr ;
let FX be Subset-Family of PT; :: thesis: ( FX is Cover of PT & FX is open implies ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite ) )
assume that
A4: FX is Cover of PT and
A5: FX is open ; :: thesis: ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )
consider R being Relation such that
A6: R well_orders FX by WELLORD2:26;
consider Mn being Relation such that
A7: Mn = R |_2 FX ;
A8: Mn well_orders FX by A6, A7, Th5;
set UB = { (union { (Ball c,(1 / 2)) where c is Element 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 Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ) where V is Subset of PM : V in FX } is Subset-Family of PM
proof
reconsider UB = { (union { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ) where V is Subset of PM : V in FX } as set ;
UB c= bool the carrier of PM
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UB or x in bool the carrier of PM )
assume x in UB ; :: thesis: x in bool the carrier of PM
then consider V being Subset of PM such that
A9: x = union { (Ball c,(1 / 2)) where c is Element 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: ( not y in x or y in the carrier of PM )
assume y in x ; :: thesis: y in the carrier of PM
then consider W being set such that
A10: y in W and
A11: W in { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } by A9, TARSKI:def 4;
consider c being Element of PM such that
A12: W = Ball c,(1 / 2) and
( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) by A11;
thus y in the carrier of PM by A10, A12; :: thesis: verum
end;
hence x in bool the carrier of PM ; :: thesis: verum
end;
hence { (union { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ) where V is Subset of PM : V in FX } is Subset-Family of PM ; :: thesis: verum
end;
then reconsider UB = { (union { (Ball c,(1 / 2)) where c is Element 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 H1( Element of PM, Element of NAT ) -> Element of bool the carrier of PM = Ball $1,(1 / (2 |^ ($2 + 1)));
defpred S1[ Element of PM, Subset of PM, Element of NAT ] means ( $1 in $2 \ (PartUnion $2,Mn) & Ball $1,(3 / (2 |^ ($3 + 1))) c= $2 );
defpred S2[ set ] means $1 in FX;
consider f being Function of NAT , bool (bool the carrier of PM) such that
A13: f . 0 = UB and
A14: for n being Element of NAT holds f . (n + 1) = { (union { H1(c,n) where c is Element of PM : ( S1[c,V,n] & not c in union { (union (f . q)) where q is Element of NAT : q <= n } ) } ) where V is Subset of PM : S2[V] } from PCOMPS_2:sch 3();
 defpred S3[ set ] means ex n being Element of NAT st $1 in f . n;
consider GX being Subset-Family of PM such that
A15: for X being Subset of PM holds
( X in GX iff S3[X] ) from SUBSET_1:sch 3();
 reconsider GX = GX as Subset-Family of PT by A1, A3, Th8;
take GX ; :: thesis: ( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )
thus A16: GX is open :: thesis: ( GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )
proof
for X being Subset of PT st X in GX holds
X is open
proof
let X be Subset of PT; :: thesis: ( X in GX implies X is open )
assume A17: X in GX ; :: thesis: X is open
then reconsider X = X as Subset of PM ;
consider n being Element of NAT such that
A18: X in f . n by A15, A17;
now
per cases ( n = 0 or n > 0 ) ;
suppose A19: n = 0 ; :: thesis: X in the topology of PT
thus X in the topology of PT :: thesis: verum
proof
consider V being Subset of PM such that
A20: X = union { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } and
V in FX by A13, A18, A19;
set NF = { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ;
{ (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } c= bool the carrier of PM
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } or a in bool the carrier of PM )
assume a in { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ; :: thesis: a in bool the carrier of PM
then consider c being Element of PM such that
A21: a = Ball c,(1 / 2) and
( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) ;
thus a in bool the carrier of PM by A21; :: thesis: verum
end;
then reconsider NF = { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } as Subset-Family of PM ;
NF c= Family_open_set PM
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in NF or a in Family_open_set PM )
assume a in NF ; :: thesis: a in Family_open_set PM
then consider c being Element of PM such that
A22: a = Ball c,(1 / 2) and
( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) ;
thus a in Family_open_set PM by A22, PCOMPS_1:33; :: thesis: verum
end;
hence X in the topology of PT by A2, A3, A20, PCOMPS_1:36; :: thesis: verum
end;
end;
suppose n > 0 ; :: thesis: X in the topology of PT
then consider k being Nat such that
A23: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
thus X in the topology of PT :: thesis: verum
proof
X in { (union { (Ball c,(1 / (2 |^ (k + 1)))) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . q)) where q is Element of NAT : q <= k } ) } ) where V is Subset of PM : V in FX } by A14, A18, A23;
then consider V being Subset of PM such that
A24: X = union { (Ball c,(1 / (2 |^ (k + 1)))) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . q)) where q is Element of NAT : q <= k } ) } and
V in FX ;
reconsider NF = { (Ball c,(1 / (2 |^ (k + 1)))) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . q)) where q is Element of NAT : q <= k } ) } as set ;
NF c= bool the carrier of PM
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in NF or a in bool the carrier of PM )
assume a in NF ; :: thesis: a in bool the carrier of PM
then consider c being Element of PM such that
A25: a = Ball c,(1 / (2 |^ (k + 1))) and
( c in V \ (PartUnion V,Mn) & Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . l)) where l is Element of NAT : l <= k } ) ;
thus a in bool the carrier of PM by A25; :: thesis: verum
end;
then reconsider NF = NF as Subset-Family of PM ;
NF c= Family_open_set PM
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in NF or a in Family_open_set PM )
assume a in NF ; :: thesis: a in Family_open_set PM
then consider c being Element of PM such that
A26: a = Ball c,(1 / (2 |^ (k + 1))) and
( c in V \ (PartUnion V,Mn) & Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . l)) where l is Element of NAT : l <= k } ) ;
thus a in Family_open_set PM by A26, PCOMPS_1:33; :: thesis: verum
end;
hence X in the topology of PT by A2, A3, A24, PCOMPS_1:36; :: thesis: verum
end;
end;
end;
end;
hence X is open by PRE_TOPC:def 5; :: thesis: verum
end;
hence GX is open by TOPS_2:def 1; :: thesis: verum
end;
thus A27: GX is Cover of PT :: thesis: ( GX is_finer_than FX & GX is locally_finite )
proof
A28: the carrier of PT c= union GX
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of PT or x in union GX )
defpred S4[ set ] means x in $1;
assume A29: x in the carrier of PT ; :: thesis: x in union GX
then ex G being Subset of PT st
( x in G & G in FX ) by A4, PCOMPS_1:5;
then A30: ex G being set st
( G in FX & S4[G] ) ;
consider X being set such that
A31: X in FX and
A32: S4[X] and
A33: for Y being set st Y in FX & S4[Y] holds
[X,Y] in Mn from PCOMPS_2:sch 1(A8, A30);
 reconsider X = X as Subset of PT by A31;
X is open by A5, A31, TOPS_2:def 1;
then A34: X in Family_open_set PM by A2, A3, PRE_TOPC:def 5;
reconsider X = X as Subset of PM by A1, A3, Th8;
reconsider x' = x as Element of PM by A1, A3, A29, Th8;
consider r being Real such that
A35: r > 0 and
A36: Ball x',r c= X by A32, A34, PCOMPS_1:def 5;
defpred S5[ Nat] means 3 / (2 |^ $1) <= r;
ex k being Element of NAT st S5[k] by A35, PREPOWER:106;
then A37: ex k being Nat st S5[k] ;
consider k being Nat such that
A38: S5[k] and
for l being Nat st S5[l] holds
k <= l from NAT_1:sch 5(A37);
 A39: k in NAT by ORDINAL1:def 13;
A40: 2 |^ k > 0 by PREPOWER:13;
2 |^ (k + 1) = (2 |^ k) * 2 by NEWTON:11;
then 2 |^ (k + 1) >= 2 |^ k by XREAL_1:153;
then A41: 3 / (2 |^ (k + 1)) <= 3 / (2 |^ k) by A40, XREAL_1:120;
assume A42: not x in union GX ; :: thesis: contradiction
A43: for V being set
for n being Element of NAT st V in f . n holds
not x in V
proof
let V be set ; :: thesis: for n being Element of NAT st V in f . n holds
not x in V
let n be Element of NAT ; :: thesis: ( V in f . n implies not x in V )
assume V in f . n ; :: thesis: not x in V
then V in GX by A15;
hence not x in V by A42, TARSKI:def 4; :: thesis: verum
end;
A44: for n being Element of NAT holds not x in union (f . n)
proof
let n be Element of NAT ; :: thesis: not x in union (f . n)
assume x in union (f . n) ; :: thesis: contradiction
then consider V being set such that
A45: ( x in V & V in f . n ) by TARSKI:def 4;
thus contradiction by A43, A45; :: thesis: verum
end;
now
set W = union { (Ball y,(1 / (2 |^ (k + 1)))) where y is Element of PM : ( y in X \ (PartUnion X,Mn) & Ball y,(3 / (2 |^ (k + 1))) c= X & not y in union { (union (f . q)) where q is Element of NAT : q <= k } ) } ;
A46: x in union { (Ball y,(1 / (2 |^ (k + 1)))) where y is Element of PM : ( y in X \ (PartUnion X,Mn) & Ball y,(3 / (2 |^ (k + 1))) c= X & not y in union { (union (f . q)) where q is Element of NAT : q <= k } ) }
proof
consider A being Subset of PM such that
A47: 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 A48: x in A by A47, TBSP_1:16;
not x' in PartUnion X,Mn
proof
assume x' in PartUnion X,Mn ; :: thesis: contradiction
then consider M being set such that
A49: x' in M and
A50: M in Mn -Seg X by TARSKI:def 4;
reconsider FX = FX as set ;
A51: ( M <> X & [M,X] in Mn ) by A50, WELLORD1:def 1;
then M in field Mn by RELAT_1:30;
then A52: M in FX by A6, A7, Th5;
then A53: [X,M] in Mn by A33, A49;
Mn is_antisymmetric_in FX by A8, WELLORD1:def 5;
hence contradiction by A31, A51, A52, A53, RELAT_2:def 4; :: thesis: verum
end;
then A54: x' in X \ (PartUnion X,Mn) by A32, XBOOLE_0:def 5;
Ball x',(3 / (2 |^ (k + 1))) c= Ball x',r by A38, A41, PCOMPS_1:1, XXREAL_0:2;
then A55: Ball x',(3 / (2 |^ (k + 1))) c= X by A36, XBOOLE_1:1;
not x' in union { (union (f . q)) where q is Element of NAT : q <= k }
proof
assume x' in union { (union (f . q)) where q is Element of NAT : q <= k } ; :: thesis: contradiction
then consider D being set such that
A56: x' in D and
A57: D in { (union (f . q)) where q is Element of NAT : q <= k } by TARSKI:def 4;
consider q being Element of NAT such that
A58: D = union (f . q) and
q <= k by A57;
thus contradiction by A44, A56, A58; :: thesis: verum
end;
then A in { (Ball y,(1 / (2 |^ (k + 1)))) where y is Element of PM : ( y in X \ (PartUnion X,Mn) & Ball y,(3 / (2 |^ (k + 1))) c= X & not y in union { (union (f . q)) where q is Element of NAT : q <= k } ) } by A47, A54, A55;
hence x in union { (Ball y,(1 / (2 |^ (k + 1)))) where y is Element of PM : ( y in X \ (PartUnion X,Mn) & Ball y,(3 / (2 |^ (k + 1))) c= X & not y in union { (union (f . q)) where q is Element of NAT : q <= k } ) } by A48, TARSKI:def 4; :: thesis: verum
end;
reconsider W = union { (Ball y,(1 / (2 |^ (k + 1)))) where y is Element of PM : ( y in X \ (PartUnion X,Mn) & Ball y,(3 / (2 |^ (k + 1))) c= X & not y in union { (union (f . q)) where q is Element of NAT : q <= k } ) } as set ;
W in { (union { (Ball y,(1 / (2 |^ (k + 1)))) where y is Element of PM : ( y in V \ (PartUnion V,Mn) & Ball y,(3 / (2 |^ (k + 1))) c= V & not y in union { (union (f . q)) where q is Element of NAT : q <= k } ) } ) where V is Subset of PM : V in FX } by A31;
then W in f . (k + 1) by A14, A39;
hence ex W being set ex l being Element of NAT st
( W in f . l & x in W ) by A46; :: thesis: verum
end;
hence contradiction by A43; :: thesis: verum
end;
the carrier of PT c= union GX by A28;
hence GX is Cover of PT by SETFAM_1:def 12; :: thesis: verum
end;
thus GX is_finer_than FX :: thesis: GX is locally_finite
proof
for X being set st X in GX holds
ex Y being set st
( Y in FX & X c= Y )
proof
let X be set ; :: thesis: ( X in GX implies ex Y being set st
( Y in FX & X c= Y ) )
assume A61: X in GX ; :: thesis: ex Y being set st
( Y in FX & X c= Y )
then reconsider X = X as Subset of PM ;
consider n being Element of NAT such that
A62: X in f . n by A15, A61;
now
per cases ( n = 0 or n > 0 ) ;
suppose A63: n = 0 ; :: thesis: ex Y being set st
( Y in FX & X c= Y )
thus ex Y being set st
( Y in FX & X c= Y ) :: thesis: verum
proof
consider V being Subset of PM such that
A64: X = union { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } and
A65: V in FX by A13, A62, A63;
set NF = { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ;
{ (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } c= bool the carrier of PM
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } or a in bool the carrier of PM )
assume a in { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } ; :: thesis: a in bool the carrier of PM
then consider c being Element of PM such that
A66: a = Ball c,(1 / 2) and
( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) ;
thus a in bool the carrier of PM by A66; :: thesis: verum
end;
then reconsider NF = { (Ball c,(1 / 2)) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / 2) c= V ) } as Subset-Family of PM ;
A67: for W being set st W in NF holds
W c= V
proof
let W be set ; :: thesis: ( W in NF implies W c= V )
assume W in NF ; :: thesis: W c= V
then consider c being Element of PM such that
A68: ( W = Ball c,(1 / 2) & c in V \ (PartUnion V,Mn) ) and
A69: Ball c,(3 / 2) c= V ;
Ball c,(1 / 2) c= Ball c,(3 / 2) by PCOMPS_1:1;
hence W c= V by A68, A69, XBOOLE_1:1; :: thesis: verum
end;
reconsider V = V as set ;
take Y = V; :: thesis: ( Y in FX & X c= Y )
thus Y in FX by A65; :: thesis: X c= Y
thus X c= Y by A64, A67, ZFMISC_1:94; :: thesis: verum
end;
end;
suppose n > 0 ; :: thesis: ex Y being set st
( Y in FX & X c= Y )
then consider k being Nat such that
A70: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
thus ex Y being set st
( Y in FX & X c= Y ) :: thesis: verum
proof
X in { (union { (Ball c,(1 / (2 |^ (k + 1)))) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . q)) where q is Element of NAT : q <= k } ) } ) where V is Subset of PM : V in FX } by A14, A62, A70;
then consider V being Subset of PM such that
A71: X = union { (Ball c,(1 / (2 |^ (k + 1)))) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . q)) where q is Element of NAT : q <= k } ) } and
A72: V in FX ;
reconsider NF = { (Ball c,(1 / (2 |^ (k + 1)))) where c is Element of PM : ( c in V \ (PartUnion V,Mn) & Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . q)) where q is Element of NAT : q <= k } ) } as set ;
NF c= bool the carrier of PM
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in NF or a in bool the carrier of PM )
assume a in NF ; :: thesis: a in bool the carrier of PM
then consider c being Element of PM such that
A73: a = Ball c,(1 / (2 |^ (k + 1))) and
( c in V \ (PartUnion V,Mn) & Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . q)) where q is Element of NAT : q <= k } ) ;
thus a in bool the carrier of PM by A73; :: thesis: verum
end;
then reconsider NF = NF as Subset-Family of PM ;
A74: for W being set st W in NF holds
W c= V
proof
let W be set ; :: thesis: ( W in NF implies W c= V )
assume W in NF ; :: thesis: W c= V
then consider c being Element of PM such that
A75: ( W = Ball c,(1 / (2 |^ (k + 1))) & c in V \ (PartUnion V,Mn) ) and
A76: ( Ball c,(3 / (2 |^ (k + 1))) c= V & not c in union { (union (f . q)) where q is Element of NAT : q <= k } ) ;
1 / (2 |^ (k + 1)) <= 3 / (2 |^ (k + 1)) by XREAL_1:74;
then Ball c,(1 / (2 |^ (k + 1))) c= Ball c,(3 / (2 |^ (k + 1))) by PCOMPS_1:1;
hence W c= V by A75, A76, XBOOLE_1:1; :: thesis: verum
end;
reconsider V = V as set ;
take Y = V; :: thesis: ( Y in FX & X c= Y )
thus Y in FX by A72; :: thesis: X c= Y
thus X c= Y by A71, A74, ZFMISC_1:94; :: thesis: verum
end;
end;
end;
end;
hence ex Y being set st
( Y in FX & X c= Y ) ; :: thesis: verum
end;
hence GX is_finer_than FX by SETFAM_1:def 2; :: thesis: verum
end;
thus GX is locally_finite :: thesis: verum
proof
for x being Point of PT ex W being Subset of PT st
( x in W & W is open & { V where V is Subset of PT : ( V in GX & V meets W ) } is finite )
proof
let x be Point of PT; :: thesis: ex W being Subset of PT st
( x in W & W is open & { V where V is Subset of PT : ( V in GX & V meets W ) } is finite )
consider X being Subset of PT such that
A77: x in X and
A78: X in GX by A27, PCOMPS_1:5;
reconsider X = X as Subset of PT ;
defpred S4[ set ] means X in f . $1;
ex n being Element of NAT st S4[n] by A15, A78;
then A79: ex n being Nat st S4[n] ;
consider k being Nat such that
A80: S4[k] and
for l being Nat st S4[l] holds
k <= l from NAT_1:sch 5(A79);
 X is open by A16, A78, TOPS_2:def 1;
then A81: X in Family_open_set PM by A2, A3, PRE_TOPC:def 5;
reconsider x' = x as Element of PM by A1, A3, Th8;
consider r being Real such that
A82: r > 0 and
A83: Ball x',r c= X by A77, A81, PCOMPS_1:def 5;
consider m being Element of NAT such that
A84: 1 / (2 |^ m) <= r by A82, PREPOWER:106;
2 |^ (((m + 1) + k) + 1) > 0 by PREPOWER:13;
then A85: 1 / (2 |^ (((m + 1) + k) + 1)) > 0 by XREAL_1:141;
consider W being Subset of PM such that
A86: W = Ball x',(1 / (2 |^ (((m + 1) + k) + 1))) ;
reconsider W = W as Subset of PT by A1, A3, Th8;
W in the topology of PT by A2, A3, A86, PCOMPS_1:33;
then A87: W is open by PRE_TOPC:def 5;
{ V where V is Subset of PT : ( V in GX & V meets W ) } is finite
proof
set NZ = { V where V is Subset of PT : ( V in GX & V meets W ) } ;
defpred S5[ set , set ] means $1 in f . $2;
A88: for p being set st p in { V where V is Subset of PT : ( V in GX & V meets W ) } holds
ex n being Element of NAT st S5[p,n]
proof
let p be set ; :: thesis: ( p in { V where V is Subset of PT : ( V in GX & V meets W ) } implies ex n being Element of NAT st S5[p,n] )
assume p in { V where V is Subset of PT : ( V in GX & V meets W ) } ; :: thesis: ex n being Element of NAT st S5[p,n]
then consider V being Subset of PT such that
A89: p = V and
A90: V in GX and
V meets W ;
consider k being Element of NAT such that
A91: V in f . k by A15, A90;
thus ex n being Element of NAT st S5[p,n] by A89, A91; :: thesis: verum
end;
consider g being Function such that
A92: dom g = { V where V is Subset of PT : ( V in GX & V meets W ) } and
A93: for y being set st y in { V where V is Subset of PT : ( V in GX & V meets W ) } holds
ex n being Element of NAT st
( g . y = n & S5[y,n] & ( for t being Element of NAT st S5[y,t] holds
n <= t ) ) from TREES_2:sch 4(A88);
 A94: rng g c= { i where i is Element of NAT : i < ((m + 1) + k) + 1 }
proof
let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in rng g or t in { i where i is Element of NAT : i < ((m + 1) + k) + 1 } )
assume t in rng g ; :: thesis: t in { i where i is Element of NAT : i < ((m + 1) + k) + 1 }
then consider a being set such that
A95: a in dom g and
A96: t = g . a by FUNCT_1:def 5;
consider n being Element of NAT such that
A97: g . a = n and
A98: a in f . n and
for p being Element of NAT st a in f . p holds
n <= p by A92, A93, A95;
assume A99: not t in { i where i is Element of NAT : i < ((m + 1) + k) + 1 } ; :: thesis: contradiction
consider V being Subset of PT such that
A100: a = V and
V in GX and
A101: V meets W by A92, A95;
reconsider t = t as Element of NAT by A96, A97;
A102: t >= ((m + 1) + k) + 1 by A99;
consider y being set such that
A103: ( y in V & y in W ) by A101, XBOOLE_0:3;
now
per cases ( t = 0 or t > 0 ) ;
suppose t > 0 ; :: thesis: contradiction
then consider l being Nat such that
A104: t = l + 1 by NAT_1:6;
reconsider l = l as Element of NAT by ORDINAL1:def 13;
V in { (union { (Ball c,(1 / (2 |^ (l + 1)))) where c is Element of PM : ( c in Y \ (PartUnion Y,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= Y & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) } ) where Y is Subset of PM : Y in FX } by A14, A96, A97, A98, A100, A104;
then consider Y being Subset of PM such that
A105: V = union { (Ball c,(1 / (2 |^ (l + 1)))) where c is Element of PM : ( c in Y \ (PartUnion Y,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= Y & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) } and
Y in FX ;
reconsider NF = { (Ball c,(1 / (2 |^ (l + 1)))) where c is Element of PM : ( c in Y \ (PartUnion Y,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= Y & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) } as set ;
consider T being set such that
A106: y in T and
A107: T in NF by A103, A105, TARSKI:def 4;
consider c being Element of PM such that
A108: T = Ball c,(1 / (2 |^ (l + 1))) and
A109: ( c in Y \ (PartUnion Y,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= Y & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) by A107;
reconsider y = y as Element of PM by A103;
A110: 2 |^ t >= 2 |^ (((m + 1) + k) + 1) by A102, PREPOWER:107;
2 |^ (((m + 1) + k) + 1) > 0 by PREPOWER:13;
then A112: 1 / (2 |^ (((m + 1) + k) + 1)) >= 1 / (2 |^ t) by A110, XREAL_1:120;
2 |^ ((1 + k) + 1) <> 0 by PREPOWER:12;
then A113: (1 / (2 |^ m)) - (1 / (2 |^ (((m + 1) + k) + 1))) = ((1 * (2 |^ ((1 + k) + 1))) / ((2 |^ m) * (2 |^ ((1 + k) + 1)))) - (1 / (2 |^ (((m + 1) + k) + 1))) by XCMPLX_1:92
.= ((1 * (2 |^ ((1 + k) + 1))) / (2 |^ (m + ((1 + k) + 1)))) - (1 / (2 |^ (((m + 1) + k) + 1))) by NEWTON:13
.= (((2 |^ (1 + k)) * 2) / (2 |^ (((m + 1) + k) + 1))) - (1 / (2 |^ (((m + 1) + k) + 1))) by NEWTON:11
.= (((2 |^ (1 + k)) * 2) - 1) / (2 |^ (((m + 1) + k) + 1)) by XCMPLX_1:121 ;
2 |^ (1 + k) >= 1 by PREPOWER:19;
then (2 |^ (1 + k)) * 2 >= 2 by XREAL_1:153;
then ((2 |^ (1 + k)) * 2) - 1 >= 2 - 1 by XREAL_1:11;
then A114: (1 / (2 |^ m)) - (1 / (2 |^ (((m + 1) + k) + 1))) >= 1 / (2 |^ (((m + 1) + k) + 1)) by A113, XREAL_1:74;
A115: for t being Element of NAT st t < l holds
not c in union (f . t)
proof
let t be Element of NAT ; :: thesis: ( t < l implies not c in union (f . t) )
assume A116: t < l ; :: thesis: not c in union (f . t)
assume A117: c in union (f . t) ; :: thesis: contradiction
union (f . t) in { (union (f . q)) where q is Element of NAT : q <= l } by A116;
hence contradiction by A109, A117, TARSKI:def 4; :: thesis: verum
end;
dist c,y < 1 / (2 |^ t) by A104, A106, A108, METRIC_1:12;
then dist c,y < 1 / (2 |^ (((m + 1) + k) + 1)) by A112, XXREAL_0:2;
then A118: (dist c,y) + (dist y,x') < (1 / (2 |^ (((m + 1) + k) + 1))) + (dist y,x') by XREAL_1:8;
A119: dist c,x' >= 1 / (2 |^ m)
proof
assume not dist c,x' >= 1 / (2 |^ m) ; :: thesis: contradiction
then dist x',c < r by A84, XXREAL_0:2;
then c in Ball x',r by METRIC_1:12;
then A120: c in union (f . k) by A80, A83, TARSKI:def 4;
A121: k <> l
proof
assume k = l ; :: thesis: contradiction
then union (f . k) in { (union (f . q)) where q is Element of NAT : q <= l } ;
hence contradiction by A109, A120, TARSKI:def 4; :: thesis: verum
end;
A122: k in NAT by ORDINAL1:def 13;
A123: l >= k + (m + 1) by A102, A104, XREAL_1:8;
k + (m + 1) >= k by NAT_1:11;
then k <= l by A123, XXREAL_0:2;
then k < l by A121, XXREAL_0:1;
hence contradiction by A115, A120, A122; :: thesis: verum
end;
(dist c,y) + (dist y,x') >= dist c,x' by METRIC_1:4;
then (dist c,y) + (dist y,x') >= 1 / (2 |^ m) by A119, XXREAL_0:2;
then (1 / (2 |^ (((m + 1) + k) + 1))) + (dist y,x') > 1 / (2 |^ m) by A118, XXREAL_0:2;
then dist y,x' >= (1 / (2 |^ m)) - (1 / (2 |^ (((m + 1) + k) + 1))) by XREAL_1:21;
then dist y,x' >= 1 / (2 |^ (((m + 1) + k) + 1)) by A114, XXREAL_0:2;
hence contradiction by A86, A103, METRIC_1:12; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
g is one-to-one
proof
for x1, x2 being set st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2
proof
let x1, x2 be set ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )
assume that
A124: x1 in dom g and
A125: x2 in dom g and
A126: g . x1 = g . x2 ; :: thesis: x1 = x2
assume A127: x1 <> x2 ; :: thesis: contradiction
consider n1 being Element of NAT such that
A128: g . x1 = n1 and
A129: x1 in f . n1 and
for t being Element of NAT st x1 in f . t holds
n1 <= t by A92, A93, A124;
consider n2 being Element of NAT such that
A130: g . x2 = n2 and
A131: x2 in f . n2 and
for t being Element of NAT st x2 in f . t holds
n2 <= t by A92, A93, A125;
consider V1 being Subset of PT such that
A132: x1 = V1 and
V1 in GX and
A133: V1 meets W by A92, A124;
consider w1 being set such that
A134: w1 in W and
A135: w1 in x1 by A132, A133, XBOOLE_0:3;
consider V2 being Subset of PT such that
A136: x2 = V2 and
V2 in GX and
A137: V2 meets W by A92, A125;
consider w2 being set such that
A138: w2 in W and
A139: w2 in x2 by A136, A137, XBOOLE_0:3;
reconsider w1 = w1, w2 = w2 as Element of PM by A134, A138;
now
per cases ( n1 = 0 or n1 > 0 ) ;
suppose A140: n1 = 0 ; :: thesis: contradiction
then consider M1 being Subset of PM such that
A141: x1 = union { (Ball c,(1 / 2)) where c is Element of PM : ( c in M1 \ (PartUnion M1,Mn) & Ball c,(3 / 2) c= M1 ) } and
A142: M1 in FX by A13, A129;
consider k1 being set such that
A143: w1 in k1 and
A144: k1 in { (Ball c,(1 / 2)) where c is Element of PM : ( c in M1 \ (PartUnion M1,Mn) & Ball c,(3 / 2) c= M1 ) } by A135, A141, TARSKI:def 4;
consider c1 being Element of PM such that
A145: k1 = Ball c1,(1 / 2) and
A146: c1 in M1 \ (PartUnion M1,Mn) and
A147: Ball c1,(3 / 2) c= M1 by A144;
consider M2 being Subset of PM such that
A148: x2 = union { (Ball c,(1 / 2)) where c is Element of PM : ( c in M2 \ (PartUnion M2,Mn) & Ball c,(3 / 2) c= M2 ) } and
A149: M2 in FX by A13, A126, A128, A130, A131, A140;
consider k2 being set such that
A150: w2 in k2 and
A151: k2 in { (Ball c,(1 / 2)) where c is Element of PM : ( c in M2 \ (PartUnion M2,Mn) & Ball c,(3 / 2) c= M2 ) } by A139, A148, TARSKI:def 4;
consider c2 being Element of PM such that
A152: k2 = Ball c2,(1 / 2) and
A153: c2 in M2 \ (PartUnion M2,Mn) and
A154: Ball c2,(3 / 2) c= M2 by A151;
A155: dist x',c2 <= (dist x',w2) + (dist w2,c2) by METRIC_1:4;
dist c1,x' <= (dist c1,w1) + (dist w1,x') by METRIC_1:4;
then A156: (dist c1,x') + (dist x',c2) <= ((dist c1,w1) + (dist w1,x')) + ((dist x',w2) + (dist w2,c2)) by A155, XREAL_1:9;
A157: dist c1,c2 <= (dist c1,x') + (dist x',c2) by METRIC_1:4;
A158: dist c1,w1 < 1 / 2 by A143, A145, METRIC_1:12;
A159: dist x',w1 < 1 / (2 |^ (((m + 1) + k) + 1)) by A86, A134, METRIC_1:12;
A160: dist x',w2 < 1 / (2 |^ (((m + 1) + k) + 1)) by A86, A138, METRIC_1:12;
A161: dist c2,w2 < 1 / 2 by A150, A152, METRIC_1:12;
dist c1,c2 <= (dist c1,w1) + ((dist w1,x') + ((dist x',w2) + (dist w2,c2))) by A156, A157, XXREAL_0:2;
then (dist c1,c2) - ((dist w1,x') + ((dist x',w2) + (dist w2,c2))) <= dist c1,w1 by XREAL_1:22;
then (dist c1,c2) - ((dist w1,x') + ((dist x',w2) + (dist w2,c2))) < 1 / 2 by A158, XXREAL_0:2;
then dist c1,c2 < (1 / 2) + ((dist w1,x') + ((dist x',w2) + (dist w2,c2))) by XREAL_1:21;
then dist c1,c2 < (dist w1,x') + ((1 / 2) + ((dist x',w2) + (dist w2,c2))) ;
then (dist c1,c2) - ((1 / 2) + ((dist x',w2) + (dist w2,c2))) < dist w1,x' by XREAL_1:21;
then (dist c1,c2) - ((1 / 2) + ((dist x',w2) + (dist w2,c2))) < 1 / (2 |^ (((m + 1) + k) + 1)) by A159, XXREAL_0:2;
then dist c1,c2 < (1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / 2) + ((dist x',w2) + (dist w2,c2))) by XREAL_1:21;
then dist c1,c2 < (dist x',w2) + ((dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) ;
then (dist c1,c2) - ((dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) < dist x',w2 by XREAL_1:21;
then (dist c1,c2) - ((dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) < 1 / (2 |^ (((m + 1) + k) + 1)) by A160, XXREAL_0:2;
then dist c1,c2 < (1 / (2 |^ (((m + 1) + k) + 1))) + ((dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) by XREAL_1:21;
then dist c1,c2 < (dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) ;
then (dist c1,c2) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) < dist w2,c2 by XREAL_1:21;
then (dist c1,c2) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) < 1 / 2 by A161, XXREAL_0:2;
then A162: dist c1,c2 < (1 / 2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) by XREAL_1:21;
A163: ((1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)) = ((1 + 1) / 2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1))))
.= (2 / 2) + (2 / (2 |^ (((m + 1) + k) + 1))) by XCMPLX_1:63 ;
A164: (m + k) + 1 >= 1 by NAT_1:11;
A165: 2 / (2 |^ (((m + 1) + k) + 1)) = (1 * 2) / ((2 |^ ((m + 1) + k)) * 2) by NEWTON:11
.= 1 / (2 |^ ((m + 1) + k)) by XCMPLX_1:92 ;
2 |^ ((m + 1) + k) >= 2 |^ 1 by A164, PREPOWER:107;
then 2 |^ ((m + 1) + k) >= 2 by NEWTON:10;
then A166: 1 / (2 |^ ((m + 1) + k)) <= 1 / 2 by XREAL_1:120;
(((1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) - (2 / 2) = 1 / (2 |^ ((m + 1) + k)) by A163, A165;
then ((1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)) <= (2 / 2) + (1 / 2) by A166, XREAL_1:22;
then A167: dist c1,c2 < 3 / 2 by A162, XXREAL_0:2;
then A168: c2 in Ball c1,(3 / 2) by METRIC_1:12;
A169: c1 in Ball c2,(3 / 2) by A167, METRIC_1:12;
A170: Mn is_connected_in FX by A8, WELLORD1:def 5;
A171: M1 <> M2 by A127, A141, A148;
hence contradiction ; :: thesis: verum
end;
suppose n1 > 0 ; :: thesis: contradiction
then consider l being Nat such that
A172: n1 = l + 1 by NAT_1:6;
reconsider l = l as Element of NAT by ORDINAL1:def 13;
x1 in { (union { (Ball c,(1 / (2 |^ (l + 1)))) where c is Element of PM : ( c in M1 \ (PartUnion M1,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= M1 & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) } ) where M1 is Subset of PM : M1 in FX } by A14, A129, A172;
then consider M1 being Subset of PM such that
A173: x1 = union { (Ball c,(1 / (2 |^ (l + 1)))) where c is Element of PM : ( c in M1 \ (PartUnion M1,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= M1 & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) } and
A174: M1 in FX ;
reconsider NF = { (Ball c,(1 / (2 |^ (l + 1)))) where c is Element of PM : ( c in M1 \ (PartUnion M1,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= M1 & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) } as set ;
consider k1 being set such that
A175: w1 in k1 and
A176: k1 in NF by A135, A173, TARSKI:def 4;
consider c1 being Element of PM such that
A177: k1 = Ball c1,(1 / (2 |^ (l + 1))) and
A178: c1 in M1 \ (PartUnion M1,Mn) and
A179: Ball c1,(3 / (2 |^ (l + 1))) c= M1 and
not c1 in union { (union (f . q)) where q is Element of NAT : q <= l } by A176;
x2 in { (union { (Ball c,(1 / (2 |^ (l + 1)))) where c is Element of PM : ( c in M2 \ (PartUnion M2,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= M2 & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) } ) where M2 is Subset of PM : M2 in FX } by A14, A126, A128, A130, A131, A172;
then consider M2 being Subset of PM such that
A180: x2 = union { (Ball c,(1 / (2 |^ (l + 1)))) where c is Element of PM : ( c in M2 \ (PartUnion M2,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= M2 & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) } and
A181: M2 in FX ;
reconsider NF = { (Ball c,(1 / (2 |^ (l + 1)))) where c is Element of PM : ( c in M2 \ (PartUnion M2,Mn) & Ball c,(3 / (2 |^ (l + 1))) c= M2 & not c in union { (union (f . q)) where q is Element of NAT : q <= l } ) } as set ;
consider k2 being set such that
A182: w2 in k2 and
A183: k2 in NF by A139, A180, TARSKI:def 4;
consider c2 being Element of PM such that
A184: k2 = Ball c2,(1 / (2 |^ (l + 1))) and
A185: c2 in M2 \ (PartUnion M2,Mn) and
A186: Ball c2,(3 / (2 |^ (l + 1))) c= M2 and
not c2 in union { (union (f . q)) where q is Element of NAT : q <= l } by A183;
A187: dist x',c2 <= (dist x',w2) + (dist w2,c2) by METRIC_1:4;
dist c1,x' <= (dist c1,w1) + (dist w1,x') by METRIC_1:4;
then A188: (dist c1,x') + (dist x',c2) <= ((dist c1,w1) + (dist w1,x')) + ((dist x',w2) + (dist w2,c2)) by A187, XREAL_1:9;
A189: dist c1,c2 <= (dist c1,x') + (dist x',c2) by METRIC_1:4;
A190: dist c1,w1 < 1 / (2 |^ (l + 1)) by A175, A177, METRIC_1:12;
A191: dist x',w1 < 1 / (2 |^ (((m + 1) + k) + 1)) by A86, A134, METRIC_1:12;
A192: dist x',w2 < 1 / (2 |^ (((m + 1) + k) + 1)) by A86, A138, METRIC_1:12;
A193: dist c2,w2 < 1 / (2 |^ (l + 1)) by A182, A184, METRIC_1:12;
dist c1,c2 <= (dist c1,w1) + ((dist w1,x') + ((dist x',w2) + (dist w2,c2))) by A188, A189, XXREAL_0:2;
then (dist c1,c2) - ((dist w1,x') + ((dist x',w2) + (dist w2,c2))) <= dist c1,w1 by XREAL_1:22;
then (dist c1,c2) - ((dist w1,x') + ((dist x',w2) + (dist w2,c2))) < 1 / (2 |^ (l + 1)) by A190, XXREAL_0:2;
then dist c1,c2 < (1 / (2 |^ (l + 1))) + ((dist w1,x') + ((dist x',w2) + (dist w2,c2))) by XREAL_1:21;
then dist c1,c2 < (dist w1,x') + ((1 / (2 |^ (l + 1))) + ((dist x',w2) + (dist w2,c2))) ;
then (dist c1,c2) - ((1 / (2 |^ (l + 1))) + ((dist x',w2) + (dist w2,c2))) < dist w1,x' by XREAL_1:21;
then (dist c1,c2) - ((1 / (2 |^ (l + 1))) + ((dist x',w2) + (dist w2,c2))) < 1 / (2 |^ (((m + 1) + k) + 1)) by A191, XXREAL_0:2;
then dist c1,c2 < (1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (l + 1))) + ((dist x',w2) + (dist w2,c2))) by XREAL_1:21;
then dist c1,c2 < (dist x',w2) + ((dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) ;
then (dist c1,c2) - ((dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) < dist x',w2 by XREAL_1:21;
then (dist c1,c2) - ((dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) < 1 / (2 |^ (((m + 1) + k) + 1)) by A192, XXREAL_0:2;
then dist c1,c2 < (1 / (2 |^ (((m + 1) + k) + 1))) + ((dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) by XREAL_1:21;
then dist c1,c2 < (dist w2,c2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) ;
then (dist c1,c2) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) < dist w2,c2 by XREAL_1:21;
then (dist c1,c2) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) < 1 / (2 |^ (l + 1)) by A193, XXREAL_0:2;
then A194: dist c1,c2 < (1 / (2 |^ (l + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) by XREAL_1:21;
A195: ((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))) = ((1 / (2 |^ (l + 1))) + (1 / (2 |^ (l + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1))))
.= ((1 + 1) / (2 |^ (l + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) by XCMPLX_1:63
.= (2 / (2 |^ (l + 1))) + (2 / (2 |^ (((m + 1) + k) + 1))) by XCMPLX_1:63 ;
n1 in rng g by A124, A128, FUNCT_1:def 5;
then n1 in { i where i is Element of NAT : i < ((m + 1) + k) + 1 } by A94;
then consider i being Element of NAT such that
A196: ( n1 = i & i < ((m + 1) + k) + 1 ) ;
consider h being Nat such that
A197: ((m + 1) + k) + 1 = (l + 1) + h by A172, A196, NAT_1:10;
h <> 0 by A172, A196, A197;
then consider i being Nat such that
A198: h = i + 1 by NAT_1:6;
A199: 2 |^ (l + 1) > 0 by PREPOWER:13;
A200: 2 / (2 |^ (((m + 1) + k) + 1)) = (1 * 2) / ((2 |^ ((l + 1) + i)) * 2) by A197, A198, NEWTON:11
.= 1 / (2 |^ ((l + 1) + i)) by XCMPLX_1:92 ;
(l + 1) + i >= l + 1 by NAT_1:11;
then 2 |^ ((l + 1) + i) >= 2 |^ (l + 1) by PREPOWER:107;
then A201: 1 / (2 |^ ((l + 1) + i)) <= 1 / (2 |^ (l + 1)) by A199, XREAL_1:120;
(((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) - (2 / (2 |^ (l + 1))) = 1 / (2 |^ ((l + 1) + i)) by A195, A200;
then ((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))) <= (2 / (2 |^ (l + 1))) + (1 / (2 |^ (l + 1))) by A201, XREAL_1:22;
then ((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))) <= (2 + 1) / (2 |^ (l + 1)) by XCMPLX_1:63;
then A202: dist c1,c2 < 3 / (2 |^ (l + 1)) by A194, XXREAL_0:2;
then A203: c2 in Ball c1,(3 / (2 |^ (l + 1))) by METRIC_1:12;
A204: c1 in Ball c2,(3 / (2 |^ (l + 1))) by A202, METRIC_1:12;
A205: Mn is_connected_in FX by A8, WELLORD1:def 5;
A206: M1 <> M2 by A127, A173, A180;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence g is one-to-one by FUNCT_1:def 8; :: thesis: verum
end;
then A207: { V where V is Subset of PT : ( V in GX & V meets W ) } , rng g are_equipotent by A92, WELLORD2:def 4;
{ i where i is Element of NAT : i < ((m + 1) + k) + 1 } is finite
proof
{ i where i is Element of NAT : i < ((m + 1) + k) + 1 } c= {0 } \/ (Seg (((m + 1) + k) + 1))
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { i where i is Element of NAT : i < ((m + 1) + k) + 1 } or x in {0 } \/ (Seg (((m + 1) + k) + 1)) )
assume x in { i where i is Element of NAT : i < ((m + 1) + k) + 1 } ; :: thesis: x in {0 } \/ (Seg (((m + 1) + k) + 1))
then consider i being Element of NAT such that
A208: x = i and
A209: i < ((m + 1) + k) + 1 ;
reconsider x1 = x as Element of NAT by A208;
now
per cases ( x1 = 0 or x1 > 0 ) ;
suppose x1 = 0 ; :: thesis: ( x1 in {0 } or x1 in Seg (((m + 1) + k) + 1) )
hence ( x1 in {0 } or x1 in Seg (((m + 1) + k) + 1) ) by TARSKI:def 1; :: thesis: verum
end;
suppose x1 > 0 ; :: thesis: ( x1 in {0 } or x1 in Seg (((m + 1) + k) + 1) )
then consider l being Nat such that
A210: x1 = l + 1 by NAT_1:6;
x1 >= 1 by A210, NAT_1:11;
hence ( x1 in {0 } or x1 in Seg (((m + 1) + k) + 1) ) by A208, A209, FINSEQ_1:3; :: thesis: verum
end;
end;
end;
hence x in {0 } \/ (Seg (((m + 1) + k) + 1)) by XBOOLE_0:def 3; :: thesis: verum
end;
hence { i where i is Element of NAT : i < ((m + 1) + k) + 1 } is finite ; :: thesis: verum
end;
then rng g is finite by A94;
hence { V where V is Subset of PT : ( V in GX & V meets W ) } is finite by A207, CARD_1:68; :: thesis: verum
end;
hence ex W being Subset of PT st
( x in W & W is open & { V where V is Subset of PT : ( V in GX & V meets W ) } is finite ) by A85, A86, A87, TBSP_1:16; :: thesis: verum
end;
hence GX is locally_finite by PCOMPS_1:def 2; :: thesis: verum
end;