let T be non empty TopSpace; :: thesis: density T c= weight T
consider B being Basis of T;
consider B1 being Basis of T such that
A1: ( B1 c= B & card B1 = weight T ) by TOPGEN_2:20;
deffunc H₁( set ) -> Element of $1 = choose $1;
defpred S₁[ set ] means $1 <> {} ;
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 set ; :: 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 = choose B2 & B2 in B1 & B2 <> {} ) ;
x in B2 by A2;
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
A3: ( W in B1 & W c= Q & W <> {} ) by Th4;
A4: choose W in A by A3;
choose W in W by A3;
hence A meets Q by A3, A4, XBOOLE_0:3; :: thesis: verum

end;

then A is dense by TOPS_1:80;
then A5: 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, A5, XBOOLE_1:1; :: thesis: verum