theorem Th3: :: WAYBEL31:3

for L1 being lower-bounded algebraic LATTICE holds CLweight L1 = card the carrier of (CompactSublatt L1)