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 [:X,Y:] 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 [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )

deffunc H1( 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 = H1(R) from PBOOLE:sch 5();
A2: rng F c= the carrier of (oContMaps (X,S))
proof
let y be object ; :: 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 object such that
A3: x in dom F and
A4: y = F . x by FUNCT_1:def 3;
reconsider x = x as Element of the topology of [:X,Y:] by A3;
A5: x is open Subset of [:X,Y:] by PRE_TOPC:def 2;
y = (x, the carrier of X) *graph by A1, A4;
then y is continuous Function of X,S by ;
then y is Element of (oContMaps (X,S)) 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 2;
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 ;
take F ; :: thesis: ( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )
thus F is monotone :: thesis: for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph
proof
let x, y be Element of (InclPoset the topology of [:X,Y:]); :: 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 [:X,Y:] by PRE_TOPC:def 2;
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 ; :: thesis: verum
end;
let W be open Subset of [:X,Y:]; :: thesis: F . W = (W, the carrier of X) *graph
W in the topology of [:X,Y:] by PRE_TOPC:def 2;
hence F . W = (W, the carrier of X) *graph by A1; :: thesis: verum