theorem :: WAYBEL14:44

for L being complete Scott TopLattice st InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) holds
ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }