defpred S1[ object , object ] means ex A, B being set st
( A = $1 & B = $2 & A c= B );
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:74;
set B1 = { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } ;
{ 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 object ; :: 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;
then A2: 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 CARD_1:11;
A3: now :: thesis: for a being object 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
ex b being object st
( b in S & S1[a,b] )
let a be object ; :: 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 object st
( b in S & S1[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 object st
( b in S & S1[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 object st
( b in S & S1[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 object 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
S1[a,f . a] from FUNCT_1:sch 6(A3);
 set G = rng f;
reconsider G = rng f as open Subset-Family of T by A4, TOPS_2:11, 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:77; :: 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 object ; :: 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 and
A7: b in S by TARSKI:def 4;
reconsider b = b as open Subset of T by A7, TOPS_2:def 1;
reconsider a = a as Point of T by A6, A7;
consider W0 being Subset of T such that
A8: W0 in B and
A9: a in W0 and
A10: W0 c= b by A6, YELLOW_9:31;
A11: W0 in { W where W is Subset of T : ( W in B & ex U being set st
( U in S & W c= U ) ) } by A7, A8, A10;
then f . W0 in G by A4, FUNCT_1:def 3;
then A12: f . W0 c= union G by ZFMISC_1:74;
S1[W0,f . W0] by A5, A11;
then W0 c= f . W0 ;
then a in f . W0 by A9;
hence a in union G by A12; :: 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 ) ) } by A4, CARD_1:12;
hence card G c= weight T by A1, A2; :: thesis: verum