let X, Y be non empty TopSpace; :: thesis: for S being Scott TopAugmentation of InclPoset the topology of Y

for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds

for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2

let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds

for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2

let W1, W2 be open Subset of [:X,Y:]; :: thesis: ( W1 c= W2 implies for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2 )

assume A1: W1 c= W2 ; :: thesis: for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2

let f1, f2 be Element of (oContMaps (X,S)); :: thesis: ( f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph implies f1 <= f2 )

assume A2: ( f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph ) ; :: thesis: f1 <= f2

reconsider g1 = f1, g2 = f2 as continuous Function of X,(Omega S) by Th1;

S is TopAugmentation of S by YELLOW_9:44;

then A3: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) by WAYBEL25:16;

A4: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;

hence f1 <= f2 by Th3; :: thesis: verum

for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds

for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2

let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds

for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2

let W1, W2 be open Subset of [:X,Y:]; :: thesis: ( W1 c= W2 implies for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2 )

assume A1: W1 c= W2 ; :: thesis: for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2

let f1, f2 be Element of (oContMaps (X,S)); :: thesis: ( f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph implies f1 <= f2 )

assume A2: ( f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph ) ; :: thesis: f1 <= f2

reconsider g1 = f1, g2 = f2 as continuous Function of X,(Omega S) by Th1;

S is TopAugmentation of S by YELLOW_9:44;

then A3: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) by WAYBEL25:16;

A4: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;

now :: thesis: for j being set st j in the carrier of X holds

ex a, b being Element of the carrier of (Omega S) st

( a = g1 . j & b = g2 . j & a <= b )

then
g1 <= g2
;ex a, b being Element of the carrier of (Omega S) st

( a = g1 . j & b = g2 . j & a <= b )

let j be set ; :: thesis: ( j in the carrier of X implies ex a, b being Element of the carrier of (Omega S) st

( a = g1 . j & b = g2 . j & a <= b ) )

assume j in the carrier of X ; :: thesis: ex a, b being Element of the carrier of (Omega S) st

( a = g1 . j & b = g2 . j & a <= b )

then reconsider x = j as Element of X ;

reconsider g1x = g1 . x, g2x = g2 . x as Element of (InclPoset the topology of Y) by A3, YELLOW_9:def 4;

take a = g1 . x; :: thesis: ex b being Element of the carrier of (Omega S) st

( a = g1 . j & b = g2 . j & a <= b )

take b = g2 . x; :: thesis: ( a = g1 . j & b = g2 . j & a <= b )

thus ( a = g1 . j & b = g2 . j ) ; :: thesis: a <= b

( g1 . x = Im (W1,x) & g2 . x = Im (W2,x) ) by A2, Def5;

then g1 . x c= g2 . x by A1, RELAT_1:124;

then g1x <= g2x by YELLOW_1:3;

hence a <= b by A4, A3, YELLOW_0:1; :: thesis: verum

end;( a = g1 . j & b = g2 . j & a <= b ) )

assume j in the carrier of X ; :: thesis: ex a, b being Element of the carrier of (Omega S) st

( a = g1 . j & b = g2 . j & a <= b )

then reconsider x = j as Element of X ;

reconsider g1x = g1 . x, g2x = g2 . x as Element of (InclPoset the topology of Y) by A3, YELLOW_9:def 4;

take a = g1 . x; :: thesis: ex b being Element of the carrier of (Omega S) st

( a = g1 . j & b = g2 . j & a <= b )

take b = g2 . x; :: thesis: ( a = g1 . j & b = g2 . j & a <= b )

thus ( a = g1 . j & b = g2 . j ) ; :: thesis: a <= b

( g1 . x = Im (W1,x) & g2 . x = Im (W2,x) ) by A2, Def5;

then g1 . x c= g2 . x by A1, RELAT_1:124;

then g1x <= g2x by YELLOW_1:3;

hence a <= b by A4, A3, YELLOW_0:1; :: thesis: verum

hence f1 <= f2 by Th3; :: thesis: verum