:: deftheorem defines CLweight WAYBEL31:def 1 :
for L1 being continuous sup-Semilattice holds CLweight L1 = meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;