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
A3: 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;
S is TopAugmentation of S by YELLOW_9:44;
then A4: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of (Omega S),the InternalRel of (Omega S) #) by WAYBEL25:16;
reconsider g1 = f1, g2 = f2 as continuous Function of X,(Omega S) by Th1;

now

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 ;
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
reconsider g1x = g1 . x, g2x = g2 . x as Element of (InclPoset the topology of Y) by A4, YELLOW_9:def 4;
( g1 . x = Im W1,x & g2 . x = Im W2,x ) by A2, Def5;
then g1 . x c= g2 . x by A1, RELAT_1:157;
then g1x <= g2x by YELLOW_1:3;
hence a <= b by A3, A4, YELLOW_0:1; :: thesis: verum

end;

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