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;

( 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 ) )

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: verumassume 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;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