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, Th26; :: thesis: L is continuous
Omega L is continuous by A1, A4, Th28;
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, Th36; :: thesis: verum