theorem :: WAYBEL23:72

for L being lower-bounded continuous LATTICE holds
( L is algebraic iff ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 )