theorem :: WAYBEL14:45
for L being complete Scott TopLattice st ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } holds
L is algebraic