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