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 H_{1}( 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_{1}(R)
from PBOOLE:sch 5();

A2: rng F c= the carrier of (oContMaps (X,S))

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

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

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

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

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

A2: rng F c= the carrier of (oContMaps (X,S))

proof

A6:
dom F = the topology of [:X,Y:]
by PARTFUN1:def 2;
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 A5, Th43;

then y is Element of (oContMaps (X,S)) by Th2;

hence y in the carrier of (oContMaps (X,S)) ; :: thesis: verum

end;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 A5, Th43;

then y is Element of (oContMaps (X,S)) by Th2;

hence y in the carrier of (oContMaps (X,S)) ; :: thesis: verum

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

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 W be open Subset of [:X,Y:]; :: thesis: F . W = (W, the carrier of X) *graph
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 A8, Th44; :: thesis: verum

end;( 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 A8, Th44; :: thesis: verum

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