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