let n be Nat; :: thesis:
let TM be metrizable TopSpace; :: thesis:
assume that
A1: ( TM is second-countable & TM is finite-ind ) and
A2: ind TM <= n ; :: thesis:
reconsider I = n as Integer ;
consider G being finite Subset-Family of TM such that
A3: G is Cover of TM and
A4: ( G is finite-ind & ind G <= 0 ) and
A5: card G <= I + 1 and
for a, b being Subset of TM st a in G & b in G & a meets b holds
a = b by A1, A2, Th7;
set cTM = the carrier of TM;
let F be finite Subset-Family of TM; :: thesis:
assume that
A6: F is open and
A7: F is Cover of TM ; :: thesis:
A8: card ((n + 1) * (card F)) = (n + 1) * (card F) ;
defpred S₁[ object , object ] means for A being Subset of TM st A = $1 holds
ex g being Function of F,(bool the carrier of TM) st
( $2 = rng g & rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) );
A9: for x being object st x in G holds
ex y being object st
( y in bool (bool the carrier of TM) & S₁[x,y] )

let x be object ; :: thesis:
assume A10: x in G ; :: thesis:
then reconsider A = x as Subset of TM ;
A11: TM | A is second-countable by A1;
[#] TM c= union F by A7, SETFAM_1:def 11;
then A c= union F ;
then A12: F is Cover of A by SETFAM_1:def 11;
( A is finite-ind & ind A <= 0 ) by A4, A10, TOPDIM_1:11;
then consider g being Function of F,(bool the carrier of TM) such that
A13: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) by A6, A11, A12, Th22;
take rng g ; :: thesis:
thus ( rng g in bool (bool the carrier of TM) & S₁[x, rng g] ) by A13; :: thesis:

end;

consider GG being Function of G,(bool (bool the carrier of TM)) such that
A14: for x being object st x in G holds
S₁[x,GG . x] from FUNCT_2:sch 1(A9);
union (rng GG) c= union (bool (bool the carrier of TM)) by ZFMISC_1:77;
then reconsider Ugg = Union GG as Subset-Family of TM ;
A15: dom GG = G by FUNCT_2:def 1;
A16: for x being object st x in dom GG holds
card (GG . x) c= card F

let x be object ; :: thesis:
assume A17: x in dom GG ; :: thesis:
then reconsider A = x as Subset of TM by A15;
consider g being Function of F,(bool the carrier of TM) such that
A18: GG . x = rng g and
rng g is open and
rng g is Cover of A and
for a being set st a in F holds
g . a c= a and
for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b by A14, A17;
dom g = F by FUNCT_2:def 1;
hence card (GG . x) c= card F by A18, CARD_1:12; :: thesis:

end;

Segm (card (dom GG)) c= Segm (n + 1) by A5, A15, NAT_1:39;
then A19: card Ugg c= (n + 1) *` (card F) by A16, CARD_2:86;
( card (card F) = card F & card (n + 1) = n + 1 ) ;
then A20: (n + 1) *` (card F) = (n + 1) * (card F) by A8, CARD_2:39;
then reconsider Ugg = Ugg as finite Subset-Family of TM by A19;
take Ugg ; :: thesis:
thus Ugg is open :: thesis:

let A be Subset of TM; :: according to TOPS_2:def 1 :: thesis:
assume A in Ugg ; :: thesis:
then consider Y being set such that
A21: A in Y and
A22: Y in rng GG by TARSKI:def 4;
consider x being object such that
A23: ( x in dom GG & Y = GG . x ) by A22, FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
ex g being Function of F,(bool the carrier of TM) st
( Y = rng g & rng g is open & rng g is Cover of x & ( for a being set st a in F holds
g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b ) ) by A14, A15, A23;
hence A is open by A21; :: thesis:

end;

[#] TM c= union Ugg

A24: [#] TM c= union G by A3, SETFAM_1:def 11;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: x in [#] TM ; :: thesis:
consider A being set such that
A26: x in A and
A27: A in G by A24, A25, TARSKI:def 4;
consider g being Function of F,(bool the carrier of TM) such that
A28: GG . A = rng g and
rng g is open and
A29: rng g is Cover of A and
for a being set st a in F holds
g . a c= a and
for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b by A14, A27;
A c= union (rng g) by A29, SETFAM_1:def 11;
then consider y being set such that
A30: x in y and
A31: y in rng g by A26, TARSKI:def 4;
GG . A in rng GG by A15, A27, FUNCT_1:def 3;
then y in Ugg by A28, A31, TARSKI:def 4;
hence x in union Ugg by A30, TARSKI:def 4; :: thesis:

end;

let A be set ; :: according to SETFAM_1:def 2 :: thesis:
assume A in Ugg ; :: thesis:
then consider Y being set such that
A32: A in Y and
A33: Y in rng GG by TARSKI:def 4;
consider x being object such that
A34: ( x in dom GG & Y = GG . x ) by A33, FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
consider g being Function of F,(bool the carrier of TM) such that
A35: Y = rng g and
rng g is open and
rng g is Cover of x and
A36: for a being set st a in F holds
g . a c= a and
for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b by A14, A15, A34;
dom g = F by FUNCT_2:def 1;
then ex z being object st
( z in F & g . z = A ) by A32, A35, FUNCT_1:def 3;
hence ex b₁ being set st
( b₁ in F & A c= b₁ ) by A36; :: thesis:

end;

Segm (card Ugg) c= Segm ((card F) * (n + 1)) by A19, A20;
hence card Ugg <= (card F) * (n + 1) by NAT_1:39; :: thesis:
defpred S₂[ object , object ] means $1 in GG . $2;

let H be finite Subset-Family of TM; :: thesis:
assume that
A37: H c= Ugg and
A38: card H > n + 1 ; :: thesis:
not H is empty by A38;
then consider XX being object such that
A39: XX in H ;
A40: for x being object st x in H holds
ex y being object st
( y in G & S₂[x,y] )

let A be object ; :: thesis:
assume A in H ; :: thesis:
then consider Y being set such that
A41: A in Y and
A42: Y in rng GG by A37, TARSKI:def 4;
ex x being object st
( x in dom GG & Y = GG . x ) by A42, FUNCT_1:def 3;
hence ex y being object st
( y in G & S₂[A,y] ) by A41; :: thesis:

end;

consider q being Function of H,G such that
A43: for x being object st x in H holds
S₂[x,q . x] from FUNCT_2:sch 1(A40);
ex y being object st
( y in G & S₂[XX,y] ) by A40, A39;
then A44: dom q = H by FUNCT_2:def 1;
assume not meet H is empty ; :: thesis:
then consider x being object such that
A45: x in meet H ;
for x1, x2 being object st x1 in dom q & x2 in dom q & q . x1 = q . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis:
assume that
A46: x1 in dom q and
A47: x2 in dom q and
A48: q . x1 = q . x2 ; :: thesis:
reconsider x1 = x1, x2 = x2 as set by TARSKI:1;
( x in x1 & x in x2 ) by A45, A46, A47, SETFAM_1:def 1;
then A49: x1 meets x2 by XBOOLE_0:3;
q . x1 in rng q by A46, FUNCT_1:def 3;
then q . x1 in G ;
then consider g being Function of F,(bool the carrier of TM) such that
A50: GG . (q . x1) = rng g and
rng g is open and
rng g is Cover of q . x1 and
for a being set st a in F holds
g . a c= a and
A51: for a, b being set st a in F & b in F & a <> b holds
g . a misses g . b by A14;
A52: dom g = F by FUNCT_2:def 1;
x2 in GG . (q . x1) by A43, A47, A48;
then A53: ex y2 being object st
( y2 in F & x2 = g . y2 ) by A50, A52, FUNCT_1:def 3;
x1 in GG . (q . x1) by A43, A46;
then ex y1 being object st
( y1 in F & x1 = g . y1 ) by A50, A52, FUNCT_1:def 3;
hence x1 = x2 by A49, A51, A53; :: thesis:

end;

end;

hence order Ugg <= n by Th3; :: thesis: