theorem Th44: :: WAYBEL23:44

for L being lower-bounded algebraic LATTICE holds the carrier of (CompactSublatt L) is with_bottom CLbasis of L