theorem :: WAYBEL23:49

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 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 ) )