let X, Y be non empty TopSpace; :: thesis: for S being Scott TopAugmentation of InclPoset the topology of Y ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps X,S) st
( F is monotone & ( for W being open Subset of holds F . W = W,the carrier of X *graph ) )
let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps X,S) st
( F is monotone & ( for W being open Subset of holds F . W = W,the carrier of X *graph ) )
deffunc H₁( Element of the topology of [:X,Y:]) -> Function = $1,the carrier of X *graph ;
consider F being ManySortedSet of the topology of [:X,Y:] such that
A1: for R being Element of the topology of [:X,Y:] holds F . R = H₁(R) from PBOOLE:sch 5();
A2: rng F c= the carrier of (oContMaps X,S)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of (oContMaps X,S) )
assume y in rng F ; :: thesis: y in the carrier of (oContMaps X,S)
then consider x being set such that
A3: x in dom F and
A4: y = F . x by FUNCT_1:def 5;
reconsider x = x as Element of the topology of [:X,Y:] by A3, PARTFUN1:def 4;
A5: x is open Subset of by PRE_TOPC:def 5;
y = x,the carrier of X *graph by A1, A4;
then y is continuous Function of X,S by A5, Th44;
then y is Element of by Th2;
hence y in the carrier of (oContMaps X,S) ; :: thesis: verum

end;

A6: dom F = the topology of [:X,Y:] by PARTFUN1:def 4;
A7: the carrier of (InclPoset the topology of [:X,Y:]) = the topology of [:X,Y:] by YELLOW_1:1;
then reconsider F = F as Function of (InclPoset the topology of [:X,Y:]),(oContMaps X,S) by A6, A2, FUNCT_2:4;
take F ; :: thesis: ( F is monotone & ( for W being open Subset of holds F . W = W,the carrier of X *graph ) )
thus F is monotone :: thesis: for W being open Subset of holds F . W = W,the carrier of X *graph

proof

let x, y be Element of ; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or F . x <= F . y )
( x in the topology of [:X,Y:] & y in the topology of [:X,Y:] ) by A7;
then reconsider W1 = x, W2 = y as open Subset of by PRE_TOPC:def 5;
assume x <= y ; :: thesis: F . x <= F . y
then A8: W1 c= W2 by YELLOW_1:3;
( F . x = W1,the carrier of X *graph & F . y = W2,the carrier of X *graph ) by A1, A7;
hence F . x <= F . y by A8, Th45; :: thesis: verum

end;

let W be open Subset of ; :: thesis: F . W = W,the carrier of X *graph
W in the topology of [:X,Y:] by PRE_TOPC:def 5;
hence F . W = W,the carrier of X *graph by A1; :: thesis: verum