:: PCOMPS_2 semantic presentation

begin

 begin


theorem Th1: :: PCOMPS_2:1
for R being Relation
for A being set st R well_orders A holds
( R |_2 A well_orders A & A = field (R |_2 A) )
proof
let R be Relation; ::_thesis: for A being set st R well_orders A holds
( R |_2 A well_orders A & A = field (R |_2 A) )
let A be set ; ::_thesis: ( R well_orders A implies ( R |_2 A well_orders A & A = field (R |_2 A) ) )
assume A1: R well_orders A ; ::_thesis: ( R |_2 A well_orders A & A = field (R |_2 A) )
then A2: R is_reflexive_in A by WELLORD1:def_5;
A3: R |_2 A is_reflexive_in A
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in A or [x,x] in R |_2 A )
assume  x in A ; ::_thesis: [x,x] in R |_2 A
then  ( [x,x] in R & [x,x] in [:A,A:] ) by A2, RELAT_2:def_1, ZFMISC_1:87;
hence  [x,x] in R |_2 A by XBOOLE_0:def_4; ::_thesis: verum
end;
A4: R |_2 A is_connected_in A
proof
let x, y be set ; :: according to RELAT_2:def_6 ::_thesis: ( not x in A or not y in A or x = y or [x,y] in R |_2 A or [y,x] in R |_2 A )
assume that
A5: ( x in A & y in A ) and
A6: x <> y ; ::_thesis: ( [x,y] in R |_2 A or [y,x] in R |_2 A )
A7: R is_connected_in A by A1, WELLORD1:def_5;
now__::_thesis:_(_(_[x,y]_in_R_&_[x,y]_in_R_|_2_A_)_or_(_[y,x]_in_R_&_[y,x]_in_R_|_2_A_)_)
percases ( [x,y] in R or [y,x] in R ) by A5, A6, A7, RELAT_2:def_6;
caseA8: [x,y] in R ; ::_thesis: [x,y] in R |_2 A
 [x,y] in [:A,A:] by A5, ZFMISC_1:87;
hence  [x,y] in R |_2 A by A8, XBOOLE_0:def_4; ::_thesis: verum
end;
caseA9: [y,x] in R ; ::_thesis: [y,x] in R |_2 A
 [y,x] in [:A,A:] by A5, ZFMISC_1:87;
hence  [y,x] in R |_2 A by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence  ( [x,y] in R |_2 A or [y,x] in R |_2 A ) ; ::_thesis: verum
end;
A10: R |_2 A c= R by XBOOLE_1:17;
A11: R |_2 A is_antisymmetric_in A
proof
let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in A or not y in A or not [x,y] in R |_2 A or not [y,x] in R |_2 A or x = y )
assume A12: ( x in A & y in A & [x,y] in R |_2 A & [y,x] in R |_2 A ) ; ::_thesis: x = y
 R is_antisymmetric_in A by A1, WELLORD1:def_5;
hence  x = y by A10, A12, RELAT_2:def_4; ::_thesis: verum
end;
A13: R |_2 A is_well_founded_in A
proof
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= A or Y = {} or ex b1 being set st
( b1 in Y & (R |_2 A) -Seg b1 misses Y ) )
assume A14: ( Y c= A & Y <> {} ) ; ::_thesis: ex b1 being set st
( b1 in Y & (R |_2 A) -Seg b1 misses Y )
 R is_well_founded_in A by A1, WELLORD1:def_5;
then consider a being set  such that
A15: ( a in Y & R -Seg a misses Y ) by A14, WELLORD1:def_3;
 (R |_2 A) -Seg a c= R -Seg a by WELLORD1:14;
hence  ex b1 being set st
( b1 in Y & (R |_2 A) -Seg b1 misses Y ) by A15, XBOOLE_1:63; ::_thesis: verum
end;
A16: A c= field (R |_2 A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in field (R |_2 A) )
assume  x in A ; ::_thesis: x in field (R |_2 A)
then  ( [x,x] in [:A,A:] & [x,x] in R ) by A2, RELAT_2:def_1, ZFMISC_1:87;
then  [x,x] in R |_2 A by XBOOLE_0:def_4;
hence  x in field (R |_2 A) by RELAT_1:15; ::_thesis: verum
end;
A17: R |_2 A is_transitive_in A
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in A or not y in A or not z in A or not [x,y] in R |_2 A or not [y,z] in R |_2 A or [x,z] in R |_2 A )
assume that
A18: x in A and
A19: y in A and
A20: z in A and
A21: ( [x,y] in R |_2 A & [y,z] in R |_2 A ) ; ::_thesis: [x,z] in R |_2 A
A22: [x,z] in [:A,A:] by A18, A20, ZFMISC_1:87;
 R is_transitive_in A by A1, WELLORD1:def_5;
then  [x,z] in R by A10, A18, A19, A20, A21, RELAT_2:def_8;
hence  [x,z] in R |_2 A by A22, XBOOLE_0:def_4; ::_thesis: verum
end;
 field (R |_2 A) c= A by WELLORD1:13;
hence  ( R |_2 A well_orders A & A = field (R |_2 A) ) by A16, A3, A17, A11, A4, A13, WELLORD1:def_5, XBOOLE_0:def_10; ::_thesis: verum
end;

scheme :: PCOMPS_2:sch 1
MinSet{ F1() ->  set , F2() ->  Relation, P1[ set ] } :
 ex X being set st
( X in F1() & P1[X] & ( for Y being set st Y in F1() & P1[Y] holds
[X,Y] in F2() ) )
provided
A1: F2() well_orders F1() and
A2: ex X being set st
( X in F1() & P1[X] )
proof
consider Y being set  such that
A3: for x being set holds
( x in Y iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch_1();
A4: ex x being set st x in Y
proof
consider x being set  such that
A5: ( x in F1() & P1[x] ) by A2;
take  x ; ::_thesis: x in Y
thus  x in Y by A3, A5; ::_thesis: verum
end;
 for x being set st x in Y holds
x in F1() by A3;
then  Y c= F1() by TARSKI:def_3;
then consider X being set  such that
A6: X in Y and
A7: for Z being set st Z in Y holds
[X,Z] in F2() by A1, A4, WELLORD1:5;
A8: for M being set st M in F1() & P1[M] holds
[X,M] in F2()
proof
let M be set ; ::_thesis: ( M in F1() & P1[M] implies [X,M] in F2() )
assume  ( M in F1() & P1[M] ) ; ::_thesis: [X,M] in F2()
then  M in Y by A3;
hence  [X,M] in F2() by A7; ::_thesis: verum
end;
 ( X in F1() & P1[X] ) by A3, A6;
hence  ex X being set st
( X in F1() & P1[X] & ( for Y being set st Y in F1() & P1[Y] holds
[X,Y] in F2() ) ) by A8; ::_thesis: verum
end;

definition
let FX be set ;
let R be Relation;
let B be Element of FX;
func PartUnion (B,R) ->  set  equals :: PCOMPS_2:def 1
 union (R -Seg B);
coherence
 union (R -Seg B) is set ;
end;

:: deftheorem  defines PartUnion PCOMPS_2:def_1_:_
 for FX being set
for R being Relation
for B being Element of FX holds PartUnion (B,R) = union (R -Seg B);

definition
let FX be set ;
let R be Relation;
func DisjointFam (FX,R) ->  set  means :: PCOMPS_2:def 2
 for A being set holds
( A in it iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) );
existence
 ex b1 being set st
for A being set holds
( A in b1 iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) )
proof
defpred S1[ set ] means  ex B being Element of FX st
( B in FX & $1 = B \ (PartUnion (B,R)) );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool (union FX) & S1[x] ) ) from XBOOLE_0:sch_1();
reconsider X = X as set ;
take  X ; ::_thesis: for A being set holds
( A in X iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) )
let A be set ; ::_thesis: ( A in X iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) )
thus  ( A in X implies ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ) by A1; ::_thesis: ( ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) implies A in X )
assume A2: ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ; ::_thesis: A in X
then  A c= union FX by XBOOLE_1:109, ZFMISC_1:74;
hence  A in X by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for A being set holds
( A in b1 iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ) ) & ( for A being set holds
( A in b2 iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex B being Element of FX st
( B in FX & $1 = B \ (PartUnion (B,R)) );
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem  defines DisjointFam PCOMPS_2:def_2_:_
 for FX being set
for R being Relation
for b3 being set holds
( b3 = DisjointFam (FX,R) iff for A being set holds
( A in b3 iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ) );

definition
let X be set ;
let n be Element of NAT ;
let f be Function of NAT,(bool X);
func PartUnionNat (n,f) ->  set  equals :: PCOMPS_2:def 3
 union (f .: ((Seg n) \ {n}));
coherence
 union (f .: ((Seg n) \ {n})) is set ;
end;

:: deftheorem  defines PartUnionNat PCOMPS_2:def_3_:_
 for X being set
for n being Element of NAT
for f being Function of NAT,(bool X) holds PartUnionNat (n,f) = union (f .: ((Seg n) \ {n}));

begin


theorem Th2: :: PCOMPS_2:2
for PT being non empty TopSpace st PT is regular holds
for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )
proof
let PT be non empty TopSpace; ::_thesis: ( PT is regular implies for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) ) )
assume A1: PT is regular ; ::_thesis: for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )
let FX be Subset-Family of PT; ::_thesis: ( FX is Cover of PT & FX is open implies ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) ) )
assume that
A2: FX is Cover of PT and
A3: FX is open ; ::_thesis: ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )
defpred S1[ set ] means  ex V1 being Subset of PT st
( V1 = $1 & V1 is open & ex W being Subset of PT st
( W in FX & Cl V1 c= W ) );
consider HX being Subset-Family of PT such that
A4: for V being Subset of PT holds
( V in HX iff S1[V] ) from SUBSET_1:sch_3();
take  HX ; ::_thesis: ( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )
 for V being Subset of PT st V in HX holds
V is open
proof
let V be Subset of PT; ::_thesis: ( V in HX implies V is open )
assume  V in HX ; ::_thesis: V is open
then  ex V1 being Subset of PT st
( V1 = V & V1 is open & ex W being Subset of PT st
( W in FX & Cl V1 c= W ) ) by A4;
hence  V is open ; ::_thesis: verum
end;
hence  HX is open by TOPS_2:def_1; ::_thesis: ( HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )
 the carrier of PT c= union HX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of PT or x in union HX )
assume  x in the carrier of PT ; ::_thesis: x in union HX
then reconsider x = x as Point of PT ;
consider V being Subset of PT such that
A5: x in V and
A6: V in FX by A2, PCOMPS_1:3;
reconsider V = V as Subset of PT ;
now__::_thesis:_x_in_union_HX
percases ( V ` <> {} or V ` = {} ) ;
supposeA7: V ` <> {} ; ::_thesis: x in union HX
 V is open by A3, A6, TOPS_2:def_1;
then A8: V ` is closed ;
 x in (V `) ` by A5;
then consider X, Y being Subset of PT such that
A9: X is open and
A10: Y is open and
A11: x in X and
A12: V ` c= Y and
A13: X misses Y by A1, A7, A8, COMPTS_1:def_2;
 ( X c= Y ` & Y ` is closed ) by A10, A13, SUBSET_1:23;
then A14: Cl X c= Y ` by TOPS_1:5;
 Y ` c= V by A12, SUBSET_1:17;
then  Cl X c= V by A14, XBOOLE_1:1;
then  X in HX by A4, A6, A9;
hence  x in union HX by A11, TARSKI:def_4; ::_thesis: verum
end;
supposeA15: V ` = {} ; ::_thesis: x in union HX
consider X being Subset of PT such that
A16: X = [#] PT ;
A17: X is open by A16;
V = ({} PT) ` by A15
.= [#] PT by PRE_TOPC:6 ;
then  Cl X = V by A16, TOPS_1:2;
then  X in HX by A4, A6, A17;
hence  x in union HX by A16, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence  x in union HX ; ::_thesis: verum
end;
hence  HX is Cover of PT by SETFAM_1:def_11; ::_thesis: for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W )
let V be Subset of PT; ::_thesis: ( V in HX implies ex W being Subset of PT st
( W in FX & Cl V c= W ) )
assume  V in HX ; ::_thesis: ex W being Subset of PT st
( W in FX & Cl V c= W )
then  ex V1 being Subset of PT st
( V1 = V & V1 is open & ex W being Subset of PT st
( W in FX & Cl V1 c= W ) ) by A4;
hence  ex W being Subset of PT st
( W in FX & Cl V c= W ) ; ::_thesis: verum
end;

theorem :: PCOMPS_2:3
for PT being non empty TopSpace
for FX being Subset-Family of PT st PT is T_2 & PT is paracompact & 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 & clf GX is_finer_than FX & GX is locally_finite )
proof
let PT be non empty TopSpace; ::_thesis: for FX being Subset-Family of PT st PT is T_2 & PT is paracompact & 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 & clf GX is_finer_than FX & GX is locally_finite )
let FX be Subset-Family of PT; ::_thesis: ( PT is T_2 & PT is paracompact & 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 & clf GX is_finer_than FX & GX is locally_finite ) )
assume that
A1: PT is T_2 and
A2: PT is paracompact and
A3: ( FX is Cover of PT & FX is open ) ; ::_thesis: ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite )
consider HX being Subset-Family of PT such that
A4: ( HX is open & HX is Cover of PT ) and
A5: for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) by A1, A2, A3, Th2, PCOMPS_1:24;
consider GX being Subset-Family of PT such that
A6: ( GX is open & GX is Cover of PT ) and
A7: GX is_finer_than HX and
A8: GX is locally_finite by A2, A4, PCOMPS_1:def_3;
A9: for V being Subset of PT st V in GX holds
ex W being Subset of PT st
( W in FX & Cl V c= W )
proof
let V be Subset of PT; ::_thesis: ( V in GX implies ex W being Subset of PT st
( W in FX & Cl V c= W ) )
assume  V in GX ; ::_thesis: ex W being Subset of PT st
( W in FX & Cl V c= W )
then consider X being set  such that
A10: X in HX and
A11: V c= X by A7, SETFAM_1:def_2;
reconsider X = X as Subset of PT by A10;
consider W being Subset of PT such that
A12: ( W in FX & Cl X c= W ) by A5, A10;
take  W ; ::_thesis: ( W in FX & Cl V c= W )
 Cl V c= Cl X by A11, PRE_TOPC:19;
hence  ( W in FX & Cl V c= W ) by A12, XBOOLE_1:1; ::_thesis: verum
end;
 clf GX is_finer_than FX
proof
let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not X in clf GX or ex b1 being set st
( b1 in FX & X c= b1 ) )
assume A13: X in clf GX ; ::_thesis: ex b1 being set st
( b1 in FX & X c= b1 )
then reconsider X = X as Subset of PT ;
consider V being Subset of PT such that
A14: X = Cl V and
A15: V in GX by A13, PCOMPS_1:def_2;
consider W being Subset of PT such that
A16: ( W in FX & Cl V c= W ) by A9, A15;
take  W ; ::_thesis: ( W in FX & X c= W )
thus  ( W in FX & X c= W ) by A14, A16; ::_thesis: verum
end;
hence  ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite ) by A6, A8; ::_thesis: verum
end;

theorem Th4: :: PCOMPS_2:4
for PT being non empty TopSpace
for PM being MetrSpace
for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
the carrier of PM = the carrier of PT
proof
let PT be non empty TopSpace; ::_thesis: for PM being MetrSpace
for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
the carrier of PM = the carrier of PT
let PM be MetrSpace; ::_thesis: for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
the carrier of PM = the carrier of PT
let f be Function of [: the carrier of PT, the carrier of PT:],REAL; ::_thesis: ( f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) implies the carrier of PM = the carrier of PT )
assume A1: f is_metric_of the carrier of PT ; ::_thesis: ( not PM = SpaceMetr ( the carrier of PT,f) or the carrier of PM = the carrier of PT )
assume  PM = SpaceMetr ( the carrier of PT,f) ; ::_thesis: the carrier of PM = the carrier of PT
then  PM = MetrStruct(# the carrier of PT,f #) by A1, PCOMPS_1:def_7;
hence  the carrier of PM = the carrier of PT ; ::_thesis: verum
end;

theorem :: PCOMPS_2:5
for PT being non empty TopSpace
for PM being MetrSpace
for FX being Subset-Family of PT
for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
( FX is Subset-Family of PT iff FX is Subset-Family of PM ) by Th4;


definition
let PM be non empty set ;
let g be Function of NAT,((bool (bool PM)) *);
let n be Element of NAT ;
:: original: .
redefine funcg . n ->  FinSequence of bool (bool PM);
coherence
 g . n is FinSequence of bool (bool PM)
proof
 g . n is Element of (bool (bool PM)) * ;
hence  g . n is FinSequence of bool (bool PM) ; ::_thesis: verum
end;
end;

scheme :: PCOMPS_2:sch 2
XXX1{ F1() ->  non empty set , F2() ->  Subset-Family of F1(), F3( set , set ) ->  Subset of F1(), P1[ set ], P2[ set , set , set , set ] } :
 ex f being Function of NAT,(bool (bool F1())) st
( f . 0 = F2() & ( for n being Element of NAT holds f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }  ) )
proof
reconsider A = <*F2()*> as Element of (bool (bool F1())) * by FINSEQ_1:def_11;
defpred S1[ Element of NAT , FinSequence of bool (bool F1()), set ] means $3 = $2 ^ <* {  (union  {  F3(c,$1) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= $1 & fq = $2 /. (q + 1) holds
P2[c,V,$1,fq]  }  ) where V is Subset of F1() : P1[V]  }  *>;
A1: for n being Element of NAT
for x being Element of (bool (bool F1())) * ex y being Element of (bool (bool F1())) * st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of (bool (bool F1())) * ex y being Element of (bool (bool F1())) * st S1[n,x,y]
let x be Element of (bool (bool F1())) * ; ::_thesis: ex y being Element of (bool (bool F1())) * st S1[n,x,y]
set T =  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }  ;
now__::_thesis:_for_X_being_set_st_X_in__{__(union__{__F3(c,n)_where_c_is_Element_of_F1()_:_for_fq_being_Subset-Family_of_F1()
for_q_being_Element_of_NAT_st_q_<=_n_&_fq_=_x_/._(q_+_1)_holds_
P2[c,V,n,fq]__}__)_where_V_is_Subset_of_F1()_:_P1[V]__}__holds_
X_in_bool_F1()
let X be set ; ::_thesis: ( X in  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }  implies X in bool F1() )
assume  X in  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }  ; ::_thesis: X in bool F1()
then consider V being Subset of F1() such that
A2: X = union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq]  }  and
 P1[V] ;
now__::_thesis:_for_a_being_set_st_a_in_X_holds_
a_in_F1()
let a be set ; ::_thesis: ( a in X implies a in F1() )
assume  a in X ; ::_thesis: a in F1()
then consider P being set  such that
A3: a in P and
A4: P in  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq]  }  by A2, TARSKI:def_4;
 ex c being Element of F1() st
( P = F3(c,n) & ( for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] ) ) by A4;
hence  a in F1() by A3; ::_thesis: verum
end;
then  X c= F1() by TARSKI:def_3;
hence  X in bool F1() ; ::_thesis: verum
end;
then reconsider T =  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }  as Subset-Family of F1() by TARSKI:def_3;
reconsider T1 = <*T*> as FinSequence of bool (bool F1()) ;
consider y being FinSequence of bool (bool F1()) such that
A5: y = x ^ T1 ;
reconsider y = y as Element of (bool (bool F1())) * by FINSEQ_1:def_11;
take  y ; ::_thesis: S1[n,x,y]
thus  S1[n,x,y] by A5; ::_thesis: verum
end;
consider g being Function of NAT,((bool (bool F1())) *) such that
A6: g . 0 = A and
A7: for n being Element of NAT holds S1[n,g . n,g . (n + 1)] from RECDEF_1:sch_2(A1);
defpred S2[ Element of NAT ] means  len (g . $1) = $1 + 1;
A8: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A9: len (g . k) = k + 1 ; ::_thesis: S2[k + 1]
len (g . (k + 1)) = len ((g . k) ^ <* {  (union  {  F3(c,k) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= k & fq = (g . k) /. (q + 1) holds
P2[c,V,k,fq]  }  ) where V is Subset of F1() : P1[V]  }  *>) by A7
.= (len (g . k)) + 1 by FINSEQ_2:16 ;
hence  S2[k + 1] by A9; ::_thesis: verum
end;
deffunc H1( Element of NAT ) ->  Element of bool (bool F1()) = (g . $1) /. (len (g . $1));
consider f being Function of NAT,(bool (bool F1())) such that
A10: for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4();
take  f ; ::_thesis: ( f . 0 = F2() & ( for n being Element of NAT holds f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }  ) )
 len <*F2()*> = 1 by FINSEQ_1:39;
hence f . 0 = <*F2()*> /. 1 by A6, A10
.= F2() by FINSEQ_4:16 ;
::_thesis: for n being Element of NAT holds f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }
let n be Element of NAT ; ::_thesis: f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }
defpred S3[ Element of NAT ] means  for q being Element of NAT st q <= $1 holds
f . q = (g . $1) /. (q + 1);
A11: S2[ 0 ] by A6, FINSEQ_1:39;
A12: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A11, A8);
then A13: (len (g . n)) + 1 = (n + 1) + 1 ;
A14: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume A15: for q being Element of NAT st q <= k holds
f . q = (g . k) /. (q + 1) ; ::_thesis: S3[k + 1]
let q be Element of NAT ; ::_thesis: ( q <= k + 1 implies f . q = (g . (k + 1)) /. (q + 1) )
assume A16: q <= k + 1 ; ::_thesis: f . q = (g . (k + 1)) /. (q + 1)
now__::_thesis:_f_._q_=_(g_._(k_+_1))_/._(q_+_1)
percases ( q = k + 1 or q < k + 1 ) by A16, XXREAL_0:1;
supposeA17: q = k + 1 ; ::_thesis: f . q = (g . (k + 1)) /. (q + 1)
thus f . q = (g . q) /. (len (g . q)) by A10
.= (g . (k + 1)) /. (q + 1) by A12, A17 ; ::_thesis: verum
end;
supposeA18: q < k + 1 ; ::_thesis: (g . (k + 1)) /. (q + 1) = f . q
A19: q + 1 >= 1 by NAT_1:11;
 q + 1 <= k + 1 by A18, NAT_1:13;
then A20: q + 1 in Seg (k + 1) by A19, FINSEQ_1:1;
then  q + 1 in Seg (len (g . k)) by A12;
then A21: q + 1 in dom (g . k) by FINSEQ_1:def_3;
A22: q <= k by A18, NAT_1:13;
 (k + 1) + 1 >= k + 1 by NAT_1:11;
then  Seg (k + 1) c= Seg ((k + 1) + 1) by FINSEQ_1:5;
then  q + 1 in Seg ((k + 1) + 1) by A20;
then  q + 1 in Seg (len (g . (k + 1))) by A12;
then  q + 1 in dom (g . (k + 1)) by FINSEQ_1:def_3;
hence (g . (k + 1)) /. (q + 1) = (g . (k + 1)) . (q + 1) by PARTFUN1:def_6
.= ((g . k) ^ <* {  (union  {  F3(c,k) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= k & fq = (g . k) /. (q + 1) holds
P2[c,V,k,fq]  }  ) where V is Subset of F1() : P1[V]  }  *>) . (q + 1) by A7
.= (g . k) . (q + 1) by A21, FINSEQ_1:def_7
.= (g . k) /. (q + 1) by A21, PARTFUN1:def_6
.= f . q by A15, A22 ;
::_thesis: verum
end;
end;
end;
hence  f . q = (g . (k + 1)) /. (q + 1) ; ::_thesis: verum
end;
deffunc H2( set ) ->  set = union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,$1,n,fq]  }  ;
deffunc H3( set ) ->  set = union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,$1,n,fq]  }  ;
set NF =  {  H3(V) where V is Subset of F1() : P1[V]  }  ;
 len (g . (n + 1)) = (n + 1) + 1 by A12;
then A23: dom (g . (n + 1)) = Seg ((n + 1) + 1) by FINSEQ_1:def_3;
A24: S3[ 0 ]
proof
let q be Element of NAT ; ::_thesis: ( q <= 0 implies f . q = (g . 0) /. (q + 1) )
assume  q <= 0 ; ::_thesis: f . q = (g . 0) /. (q + 1)
then A25: q = 0 ;
thus f . q = (g . q) /. (len (g . q)) by A10
.= (g . 0) /. (q + 1) by A6, A25, FINSEQ_1:39 ; ::_thesis: verum
end;
A26: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A24, A14);
A27: for V being Subset of F1() st P1[V] holds
H3(V) = H2(V)
proof
deffunc H4( set ) ->  Subset of F1() = F3($1,n);
let V be Subset of F1(); ::_thesis: ( P1[V] implies H3(V) = H2(V) )
assume  P1[V] ; ::_thesis: H3(V) = H2(V)
defpred S4[ set ] means  for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[$1,V,n,fq];
defpred S5[ set ] means  for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = (g . n) /. (q + 1) holds
P2[$1,V,n,fq];
A28: for c being Element of F1() holds
( S4[c] iff S5[c] )
proof
let c be Element of F1(); ::_thesis: ( S4[c] iff S5[c] )
thus  ( ( for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq] ) implies for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq] ) ::_thesis: ( S5[c] implies S4[c] )
proof
assume A29: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq] ; ::_thesis: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq]
let fq be Subset-Family of F1(); ::_thesis: for q being Element of NAT st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq]
let q be Element of NAT ; ::_thesis: ( q <= n & fq = (g . n) /. (q + 1) implies P2[c,V,n,fq] )
assume that
A30: q <= n and
A31: fq = (g . n) /. (q + 1) ; ::_thesis: P2[c,V,n,fq]
 fq = f . q by A26, A30, A31;
hence  P2[c,V,n,fq] by A29, A30; ::_thesis: verum
end;
assume A32: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq] ; ::_thesis: S4[c]
let fq be Subset-Family of F1(); ::_thesis: for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq]
let q be Element of NAT ; ::_thesis: ( q <= n & fq = f . q implies P2[c,V,n,fq] )
assume that
A33: q <= n and
A34: fq = f . q ; ::_thesis: P2[c,V,n,fq]
 f . q = (g . n) /. (q + 1) by A26, A33;
hence  P2[c,V,n,fq] by A32, A33, A34; ::_thesis: verum
end;
  {  H4(c) where c is Element of F1() : S4[c]  }  =  {  H4(c) where c is Element of F1() : S5[c]  }  from FRAENKEL:sch_3(A28);
hence  H3(V) = H2(V) ; ::_thesis: verum
end;
A35:  {  H3(V) where V is Subset of F1() : P1[V]  }  =  {  H2(V) where V is Subset of F1() : P1[V]  }  from FRAENKEL:sch_6(A27);
then  len (g . (n + 1)) = len ((g . n) ^ <* {  H3(V) where V is Subset of F1() : P1[V]  }  *>) by A7
.= (len (g . n)) + 1 by FINSEQ_2:16 ;
hence f . (n + 1) = (g . (n + 1)) /. ((len (g . n)) + 1) by A10
.= (g . (n + 1)) . ((len (g . n)) + 1) by A23, A13, FINSEQ_1:4, PARTFUN1:def_6
.= ((g . n) ^ <* {  H3(V) where V is Subset of F1() : P1[V]  }  *>) . ((len (g . n)) + 1) by A7, A35
.=  {  H3(V) where V is Subset of F1() : P1[V]  }  by FINSEQ_1:42 ;
::_thesis: verum
end;

scheme :: PCOMPS_2:sch 3
XXX{ F1() ->  non empty set , F2() ->  Subset-Family of F1(), F3( set , set ) ->  Subset of F1(), P1[ set ], P2[ set , set , set ] } :
 ex f being Function of NAT,(bool (bool F1())) st
( f . 0 = F2() & ( for n being Element of NAT holds f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  )  }  ) where V is Subset of F1() : P1[V]  }  ) )
proof
defpred S1[ set , set , set , set ] means ( P2[$1,$2,$3] & not $1 in union $4 );
consider f being Function of NAT,(bool (bool F1())) such that
A1: f . 0 = F2() and
A2: for n being Element of NAT holds f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
S1[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }  from PCOMPS_2:sch_2();
take  f ; ::_thesis: ( f . 0 = F2() & ( for n being Element of NAT holds f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  )  }  ) where V is Subset of F1() : P1[V]  }  ) )
thus  f . 0 = F2() by A1; ::_thesis: for n being Element of NAT holds f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  )  }  ) where V is Subset of F1() : P1[V]  }
let n be Element of NAT ; ::_thesis: f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  )  }  ) where V is Subset of F1() : P1[V]  }
deffunc H1( set ) ->  set = union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
( P2[c,$1,n] & not c in union fq )  }  ;
deffunc H2( set ) ->  set = union  {  F3(c,n) where c is Element of F1() : ( P2[c,$1,n] & not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  )  }  ;
set fxxx1 =  {  H1(V) where V is Subset of F1() : P1[V]  }  ;
set fxxx =  {  H2(V) where V is Subset of F1() : P1[V]  }  ;
A3: now__::_thesis:_for_V_being_Subset_of_F1()_st_P1[V]_holds_
H1(V)_=_H2(V)
deffunc H3( set ) ->  Subset of F1() = F3($1,n);
let V be Subset of F1(); ::_thesis: ( P1[V] implies H1(V) = H2(V) )
assume  P1[V] ; ::_thesis: H1(V) = H2(V)
defpred S2[ set ] means  for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
( P2[$1,V,n] & not $1 in union fq );
defpred S3[ set ] means ( P2[$1,V,n] & not $1 in union  {  (union (f . q1)) where q1 is Element of NAT : q1 <= n  }  );
A4: now__::_thesis:_for_c_being_Element_of_F1()_holds_
(_S2[c]_iff_S3[c]_)
let c be Element of F1(); ::_thesis: ( S2[c] iff S3[c] )
A5: ( ( for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq ) iff not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  )
proof
thus  ( ( for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq ) implies not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  ) ::_thesis: ( not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  implies for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq )
proof
assume A6: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq ; ::_thesis: not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }
assume  c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  ; ::_thesis: contradiction
then consider C being set  such that
A7: c in C and
A8: C in  {  (union (f . q)) where q is Element of NAT : q <= n  }  by TARSKI:def_4;
 ex q being Element of NAT st
( C = union (f . q) & q <= n ) by A8;
hence  contradiction by A6, A7; ::_thesis: verum
end;
assume A9: not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  ; ::_thesis: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq
let fq be Subset-Family of F1(); ::_thesis: for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq
let q be Element of NAT ; ::_thesis: ( q <= n & fq = f . q implies not c in union fq )
assume  ( q <= n & fq = f . q ) ; ::_thesis: not c in union fq
then A10: union fq in  {  (union (f . p)) where p is Element of NAT : p <= n  }  ;
assume  c in union fq ; ::_thesis: contradiction
hence  contradiction by A9, A10, TARSKI:def_4; ::_thesis: verum
end;
thus  ( S2[c] iff S3[c] ) ::_thesis: verum
proof
hereby  ::_thesis: ( S3[c] implies S2[c] )
consider q being Element of NAT  such that
A11: q <= n ;
assume A12: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
( P2[c,V,n] & not c in union fq ) ; ::_thesis: ( P2[c,V,n] & not c in union  {  (union (f . p)) where p is Element of NAT : p <= n  }  )
 ex fq being Subset-Family of F1() st fq = f . q ;
hence  P2[c,V,n] by A12, A11; ::_thesis: not c in union  {  (union (f . p)) where p is Element of NAT : p <= n  }
thus  not c in union  {  (union (f . p)) where p is Element of NAT : p <= n  }  by A5, A12; ::_thesis: verum
end;
assume  ( P2[c,V,n] & not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  ) ; ::_thesis: S2[c]
hence  S2[c] by A5; ::_thesis: verum
end;
end;
  {  H3(c) where c is Element of F1() : S2[c]  }  =  {  H3(c) where c is Element of F1() : S3[c]  }  from FRAENKEL:sch_3(A4);
hence  H1(V) = H2(V) ; ::_thesis: verum
end;
  {  H1(V) where V is Subset of F1() : P1[V]  }  =  {  H2(V) where V is Subset of F1() : P1[V]  }  from FRAENKEL:sch_6(A3);
hence  f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  )  }  ) where V is Subset of F1() : P1[V]  }  by A2; ::_thesis: verum
end;

theorem Th6: :: PCOMPS_2:6
for PT being non empty TopSpace st PT is metrizable holds
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 )
proof
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, Element of NAT ) ->  Element of bool the carrier of PM = Ball ($1,(1 / (2 |^ ($2 + 1))));
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
A8: 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
A9: y in W and
A10: 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 A8, TARSKI:def_4;
 ex c being Element of PM st
( W = Ball (c,(1 / 2)) & 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,(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 ;
defpred S2[ Element of PM, Subset of PM, Element of NAT ] means ( $1 in $2 \ (PartUnion ($2,Mn)) & Ball ($1,(3 / (2 |^ ($3 + 1)))) c= $2 );
consider f being Function of NAT,(bool (bool the carrier of PM)) such that
A11: f . 0 = UB and
A12: for n being Element of 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 Element of NAT : q <= n  }  )  }  ) where V is Subset of PM : S1[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
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 Element of NAT  such that
A16: X in f . n by A13, A15;
now__::_thesis:_X_in_the_topology_of_PT
percases ( n = 0 or n > 0 ) ;
supposeA17: 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,(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 A11, A16, A17;
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  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 ;
 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  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 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 Element of 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 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  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 Element of 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 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  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 Element of 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 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 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 Element of 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 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 A13;
hence  not x in V by A33, TARSKI:def_4; ::_thesis: verum
end;
A35: 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  ex V being set st
( x in V & V in f . n ) by TARSKI:def_4;
hence  contradiction by A34; ::_thesis: verum
end;
A36: k in NAT by ORDINAL1:def_12;
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 Element of 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 Element of NAT : q <= k  }  )  }
proof
A38: not x9 in union  {  (union (f . q)) where q is Element of NAT : q <= k  }
proof
assume  x9 in union  {  (union (f . q)) where q is Element of 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 Element of NAT : q <= k  }  by TARSKI:def_4;
 ex q being Element of NAT st
( D = union (f . q) & q <= k ) by A40;
hence  contradiction by A35, 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, WELLORD1:def_5;
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, RELAT_2:def_4; ::_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, XBOOLE_1:1;
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 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 Element of 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 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 A24;
then  W in f . (k + 1) by A12, A36;
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 Element of NAT  such that
A52: X in f . n by A13, A51;
now__::_thesis:_ex_Y_being_set_st_
(_Y_in_FX_&_X_c=_Y_)
percases ( n = 0 or n > 0 ) ;
supposeA53: 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 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  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, 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 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 Element of 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 Element of 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 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  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 Element of 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 Element of 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, 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 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 by SETFAM_1:def_2; ::_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 Element of NAT  such that
A69: 1 / (2 |^ m) <= r by A67, PREPOWER:92;
defpred S4[ set ] means X in f . $1;
 ex n being Element of 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[ set , 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 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  ex V being Subset of PT st
( p = V & V in GX & V meets W ) ;
hence  ex n being Element of 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 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(A74);
A77: 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
A78: a in dom g and
A79: t = g . a by FUNCT_1:def_3;
assume A80: not t in  {  i where i is Element of NAT : i < ((m + 1) + k) + 1  }  ; ::_thesis: contradiction
A81: ex n being Element of NAT st
( g . a = n & a in f . n & ( for p being Element of NAT st a in f . p holds
n <= p ) ) by A75, A76, A78;
then reconsider t = t as Element of NAT by A79;
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 set  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
percases ( t = 0 or t > 0 ) ;
suppose t = 0 ; ::_thesis: contradiction
hence  contradiction by A80; ::_thesis: verum
end;
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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 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
A103: x1 in dom g and
A104: x2 in dom g and
A105: g . x1 = g . x2 ; ::_thesis: x1 = x2
 ex V2 being Subset of PT st
( x2 = V2 & V2 in GX & V2 meets W ) by A75, A104;
then consider w2 being set  such that
A106: w2 in W and
A107: w2 in x2 by XBOOLE_0:3;
consider n1 being Element of NAT  such that
A108: g . x1 = n1 and
A109: x1 in f . n1 and
 for t being Element of 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 set  such that
A110: w1 in W and
A111: w1 in x1 by XBOOLE_0:3;
assume A112: x1 <> x2 ; ::_thesis: contradiction
reconsider w1 = w1, w2 = w2 as Element of PM by A110, A106;
A113: ex n2 being Element of NAT st
( g . x2 = n2 & x2 in f . n2 & ( for t being Element of NAT st x2 in f . t holds
n2 <= t ) ) by A75, A76, A104;
now__::_thesis:_contradiction
percases ( n1 = 0 or n1 > 0 ) ;
supposeA114: 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 by NEWTON:5;
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, WELLORD1:def_5;
A119: dist (x9,w2) < 1 / (2 |^ (((m + 1) + k) + 1)) by A72, A106, 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, A109, 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 A111, 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, A108, 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 A107, 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, A110, 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 A112, A120, A128;
A141: c2 in Ball (c1,(3 / 2)) by A138, METRIC_1:11;
now__::_thesis:_contradiction
percases ( [M1,M2] in Mn or [M2,M1] in Mn ) by A121, A129, A118, A140, RELAT_2:def_6;
suppose [M1,M2] in Mn ; ::_thesis: contradiction
then  M1 in Mn -Seg M2 by A140, WELLORD1:1;
then  c2 in PartUnion (M2,Mn) by A126, A141, TARSKI:def_4;
hence  contradiction by A133, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose [M2,M1] in Mn ; ::_thesis: contradiction
then  M2 in Mn -Seg M1 by A140, WELLORD1:1;
then  c1 in PartUnion (M1,Mn) by A134, A139, TARSKI:def_4;
hence  contradiction by A125, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
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 Element of NAT : q <= l  }  )  }  ) where M1 is Subset of PM : M1 in FX  }  by A12, A109, A142;
A144: dist (x9,w2) < 1 / (2 |^ (((m + 1) + k) + 1)) by A72, A106, 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 Element of NAT : q <= l  }  )  }  ) where M2 is Subset of PM : M2 in FX  }  by A12, A105, A108, 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, A108, FUNCT_1:def_3;
then  n1 in  {  i where i is Element of NAT : i < ((m + 1) + k) + 1  }  by A77;
then A147: ex i being Element of 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, WELLORD1:def_5;
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 Element of 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 Element of NAT : q <= l  }  )  }  as set ;
consider k1 being set  such that
A155: w1 in k1 and
A156: k1 in NF by A111, 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 Element of 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 Element of NAT : q <= l  }  )  }  and
A162: M2 in FX by A145;
A163: M1 <> M2 by A112, 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 Element of NAT : q <= l  }  )  }  as set ;
consider k2 being set  such that
A164: w2 in k2 and
A165: k2 in NF by A107, 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 Element of 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, A110, 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;
now__::_thesis:_contradiction
percases ( [M1,M2] in Mn or [M2,M1] in Mn ) by A154, A162, A152, A163, RELAT_2:def_6;
suppose [M1,M2] in Mn ; ::_thesis: contradiction
then  M1 in Mn -Seg M2 by A163, WELLORD1:1;
then  c2 in PartUnion (M2,Mn) by A159, A174, TARSKI:def_4;
hence  contradiction by A167, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose [M2,M1] in Mn ; ::_thesis: contradiction
then  M2 in Mn -Seg M1 by A163, WELLORD1:1;
then  c1 in PartUnion (M1,Mn) by A168, A173, TARSKI:def_4;
hence  contradiction by A158, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
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 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 A176: ex i being Element of NAT st
( x = i & i < ((m + 1) + k) + 1 ) ;
then reconsider x1 = x as Element of NAT ;
now__::_thesis:_(_x1_in_{0}_or_x1_in_Seg_(((m_+_1)_+_k)_+_1)_)
percases ( 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 Element of 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
end;

theorem :: PCOMPS_2:7
for PT being non empty TopSpace st PT is metrizable holds
PT is paracompact
proof
let PT be non empty TopSpace; ::_thesis: ( PT is metrizable implies PT is paracompact )
assume  PT is metrizable ; ::_thesis: PT is paracompact
then  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 ) by Th6;
hence  PT is paracompact by PCOMPS_1:def_3; ::_thesis: verum
end;