let T be non empty TopSpace; :: thesis:
defpred S1[ set ] means \$1 <> {} ;
deffunc H1( set ) -> Element of \$1 = the Element of \$1;
set B = the Basis of T;
consider B1 being Basis of T such that
B1 c= the Basis of T and
A1: card B1 = weight T by TOPGEN_2:18;
set A = { H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } ;
{ H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } c= the carrier of T
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } or x in the carrier of T )
assume x in { H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } ; :: thesis: x in the carrier of T
then consider B2 being Subset of T such that
A2: x = the Element of B2 and
B2 in B1 and
A3: B2 <> {} ;
x in B2 by A2, A3;
hence x in the carrier of T ; :: thesis: verum
end;
then reconsider A = { H1(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S1[BB] ) } as Subset of T ;
for Q being Subset of T st Q <> {} & Q is open holds
A meets Q
proof
let Q be Subset of T; :: thesis: ( Q <> {} & Q is open implies A meets Q )
assume ( Q <> {} & Q is open ) ; :: thesis: A meets Q
then consider W being Subset of T such that
A4: W in B1 and
A5: W c= Q and
A6: W <> {} by Th4;
( the Element of W in A & the Element of W in W ) by A4, A6;
hence A meets Q by ; :: thesis: verum
end;
then A is dense by TOPS_1:45;
then A7: density T c= card A by TOPGEN_1:def 12;
card { H1(w) where w is Element of bool the carrier of T : ( w in B1 & S1[w] ) } c= card B1 from hence density T c= weight T by A1, A7; :: thesis: verum