let X, Y be non empty TopSpace; :: thesis: for S being Scott TopAugmentation of InclPoset the topology of Y
for f1, f2 being Element of (ContMaps X,S) st f1 <= f2 holds
*graph f1 c= *graph f2
let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for f1, f2 being Element of (ContMaps X,S) st f1 <= f2 holds
*graph f1 c= *graph f2
let f1, f2 be Element of (ContMaps X,S); :: thesis: ( f1 <= f2 implies *graph f1 c= *graph f2 )
assume A1: f1 <= f2 ; :: thesis: *graph f1 c= *graph f2
let a, b be set ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in *graph f1 or [a,b] in *graph f2 )
assume A2: [a,b] in *graph f1 ; :: thesis: [a,b] in *graph f2
( f1 is Function of X,S & f2 is Function of X,S ) by WAYBEL24:21;
then A3: ( dom f1 = the carrier of X & dom f2 = the carrier of X ) by FUNCT_2:def 1;
A4: ( a in dom f1 & b in f1 . a ) by A2, WAYBEL26:39;
reconsider a' = a as Element of X by A2, A3, WAYBEL26:39;
A5: 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;
reconsider F1 = f1, F2 = f2 as Function of X,S by WAYBEL24:21;
F1 . a' is Element of S ;
then f1 . a in the carrier of (InclPoset the topology of Y) by A5;
then A6: f1 . a in the topology of Y by YELLOW_1:1;
F2 . a' is Element of S ;
then f2 . a in the carrier of (InclPoset the topology of Y) by A5;
then A7: f2 . a in the topology of Y by YELLOW_1:1;
[(f1 . a'),(f2 . a')] in the InternalRel of S by A1, WAYBEL24:20;
then [(f1 . a),(f2 . a)] in RelIncl the topology of Y by A5, YELLOW_1:1;
then f1 . a c= f2 . a by A6, A7, WELLORD2:def 1;
hence [a,b] in *graph f2 by A3, A4, WAYBEL26:39; :: thesis: verum