theorem Th13: :: WAYBEL31:13

for L1 being finite LATTICE
for B1 being with_bottom CLbasis of L1 holds
( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) )