let L be complete Scott TopLattice; :: thesis: ( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) )
InclPoset (sigma L) = InclPoset the topology of L by Th23;
hence ( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) ) by WAYBEL_6:39; :: thesis: verum