let T be non empty TopSpace; :: thesis: density T c= weight T
defpred S₁[ set ] means $1 <> {} ;
deffunc H₁( 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 = { H₁(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S₁[BB] ) } ;
{ H₁(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S₁[BB] ) } c= the carrier of T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S₁[BB] ) } or x in the carrier of T )
assume x in { H₁(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S₁[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 = { H₁(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S₁[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 A5, XBOOLE_0:3; :: thesis: verum

end;

then A is dense by TOPS_1:45;
then A7: density T c= card A by TOPGEN_1:def 12;
card { H₁(w) where w is Element of bool the carrier of T : ( w in B1 & S₁[w] ) } c= card B1 from BORSUK_2:sch 1();
hence density T c= weight T by A1, A7; :: thesis: verum