let T be empty TopSpace; :: thesis: weight T is empty
reconsider B = {} as empty Subset-Family of T by TOPGEN_4:18;
( B c= the topology of T & ( for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ) ) ;
then reconsider B = B as Basis of T by YELLOW_9:32;
weight T c= card B by WAYBEL23:73;
hence weight T is empty ; :: thesis: verum