let L be complete Scott TopLattice; :: thesis: ( ( ( 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 ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive )
InclPoset (sigma L) = InclPoset the topology of L by Th23;
hence ( ( ( 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 ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive ) by WAYBEL_6:38; :: thesis: verum