let X be non empty TopSpace; :: thesis: for L being non trivial complete Scott TopLattice holds
( oContMaps X,L is complete & oContMaps X,L is continuous iff ( InclPoset the topology of X is continuous & L is continuous ) )
let L be non trivial complete Scott TopLattice; :: thesis: ( oContMaps X,L is complete & oContMaps X,L is continuous iff ( InclPoset the topology of X is continuous & L is continuous ) )
A1: L is Scott TopAugmentation of L by YELLOW_9:44;
Omega L = TopRelStr(# the carrier of L,the InternalRel of L,the topology of L #) by WAYBEL25:15;
then A2: RelStr(# the carrier of (Omega L),the InternalRel of (Omega L) #) = RelStr(# the carrier of L,the InternalRel of L #) ;
A3: L is monotone-convergence by WAYBEL25:29;

hereby :: thesis: ( InclPoset the topology of X is continuous & L is continuous implies ( oContMaps X,L is complete & oContMaps X,L is continuous ) )

assume A4: ( oContMaps X,L is complete & oContMaps X,L is continuous ) ; :: thesis: ( InclPoset the topology of X is continuous & L is continuous )
hence InclPoset the topology of X is continuous by A3, Th27; :: thesis: L is continuous
Omega L is continuous by A1, A4, Th29;
hence L is continuous by A2, YELLOW12:15; :: thesis: verum

end;

thus ( InclPoset the topology of X is continuous & L is continuous implies ( oContMaps X,L is complete & oContMaps X,L is continuous ) ) by A1, Th37; :: thesis: verum