theorem Th9: :: WAYBEL31:9

for T being TopStruct
for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 & T is finite holds
CLweight L1 = card the carrier of L1