let T be non empty TopSpace; :: thesis: for S being open Subset-Family of T ex G being open Subset-Family of T st
( G c= S & union G = union S & card G c= weight T )
let S be open Subset-Family of T; :: thesis: ex G being open Subset-Family of T st
( G c= S & union G = union S & card G c= weight T )
consider B being Basis of T such that
A1: card B = weight T by WAYBEL23:75;
set B1 = { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } ;
A2: { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } c= B

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } or a in B )
assume a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } ; :: thesis: a in B
then ex W being Subset of T st
( a = W & W in B & ex U being set st
( U in S & W c= U ) ) ;
hence a in B ; :: thesis: verum

end;

defpred S₁[ set , set ] means $1 c= $2;

A3: now

let a be set ; :: thesis: ( a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } implies ex b being set st
( b in S & S₁[a,b] ) )
assume a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } ; :: thesis: ex b being set st
( b in S & S₁[a,b] )
then ex W being Subset of T st
( a = W & W in B & ex U being set st
( U in S & W c= U ) ) ;
hence ex b being set st
( b in S & S₁[a,b] ) ; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } & rng f c= S ) and
A5: for a being set st a in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } holds
S₁[a,f . a] from WELLORD2:sch 1(A3);
set G = rng f;
reconsider G = rng f as open Subset-Family of T by A4, TOPS_2:18, XBOOLE_1:1;
take G ; :: thesis: ( G c= S & union G = union S & card G c= weight T )
thus ( G c= S & union G c= union S ) by A4, ZFMISC_1:95; :: according to XBOOLE_0:def 10 :: thesis: ( union S c= union G & card G c= weight T )
thus union S c= union G :: thesis: card G c= weight T

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in union S or a in union G )
assume a in union S ; :: thesis: a in union G
then consider b being set such that
A6: ( a in b & b in S ) by TARSKI:def 4;
reconsider a = a as Point of T by A6;
reconsider b = b as open Subset of T by A6, TOPS_2:def 1;
consider W0 being Subset of T such that
A7: ( W0 in B & a in W0 & W0 c= b ) by A6, YELLOW_9:31;
W0 in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } by A6, A7;
then ( W0 c= f . W0 & f . W0 in G ) by A4, A5, FUNCT_1:def 5;
then ( a in f . W0 & f . W0 c= union G ) by A7, ZFMISC_1:92;
hence a in union G ; :: thesis: verum

end;

( card G c= card { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } & card { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } c= card B ) by A2, A4, CARD_1:27, CARD_1:28;
hence card G c= weight T by A1, XBOOLE_1:1; :: thesis: verum