let T be non empty discrete TopStruct ; :: thesis: weight T = card the carrier of T
set M = { (card C) where C is Basis of T : verum } ;
reconsider B0 = SmallestPartition the carrier of T as Basis of T by Th13;
A1: card B0 in { (card C) where C is Basis of T : verum } ;
A2: card B0 = card the carrier of T by Th12;
weight T = meet { (card C) where C is Basis of T : verum } by WAYBEL23:def 5;
hence weight T c= card the carrier of T by A2, A1, SETFAM_1:3; :: according to XBOOLE_0:def 10 :: thesis: card the carrier of T c= weight T
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence card the carrier of T c= weight T by A2, Th13, CARD_1:11; :: thesis: verum