theorem :: WAYBEL14:41

for L being complete Scott TopLattice holds
( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) )