theorem Th48: :: WAYBEL23:48

for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) )