let T be non empty discrete TopStruct ; :: thesis: weight T = card the carrier of T
consider B being Basis of T such that
A1: card B = weight T by WAYBEL23:75;
reconsider B0 = SmallestPartition the carrier of T as Basis of T by Th14;
A2: card B0 = card the carrier of T by Th13;
set M = { (card C) where C is Basis of T : verum } ;
A3: weight T = meet { (card C) where C is Basis of T : verum } by WAYBEL23:def 5;
card B0 in { (card C) where C is Basis of T : verum } ;
hence weight T c= card the carrier of T by A2, A3, SETFAM_1:4; :: according to XBOOLE_0:def 10 :: thesis: card the carrier of T c= weight T
thus card the carrier of T c= weight T by A1, A2, Th14, CARD_1:27; :: thesis: verum