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;

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 )

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;

then g1 <= g2 ;
hence f1 <= f2 by Th3; :: thesis: verum