:: deftheorem defines weight WAYBEL23:def 5 :
for T being TopStruct holds weight T = meet { (card B) where B is Basis of T : verum } ;