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

reconsider F1 = f1, F2 = f2 as Function of X,S by WAYBEL24:21;

let a, b be object ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in *graph f1 or [a,b] in *graph f2 )

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

f2 is Function of X,S by WAYBEL24:21;

then A3: dom f2 = the carrier of X by FUNCT_2:def 1;

assume A4: [a,b] in *graph f1 ; :: thesis: [a,b] in *graph f2

then A5: ( a in dom f1 & b in f1 . a ) by WAYBEL26:38;

f1 is Function of X,S by WAYBEL24:21;

then A6: dom f1 = the carrier of X by FUNCT_2:def 1;

then reconsider a9 = a as Element of X by A4, WAYBEL26:38;

F1 . a9 is Element of S ;

then f1 . a in the carrier of (InclPoset the topology of Y) by A2;

then A7: f1 . a in the topology of Y by YELLOW_1:1;

F2 . a9 is Element of S ;

then f2 . a in the carrier of (InclPoset the topology of Y) by A2;

then A8: f2 . a in the topology of Y by YELLOW_1:1;

[(f1 . a9),(f2 . a9)] in the InternalRel of S by A1, WAYBEL24:20;

then [(f1 . a),(f2 . a)] in RelIncl the topology of Y by A2, YELLOW_1:1;

then f1 . a c= f2 . a by A7, A8, WELLORD2:def 1;

hence [a,b] in *graph f2 by A6, A3, A5, WAYBEL26:38; :: thesis: verum

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

reconsider F1 = f1, F2 = f2 as Function of X,S by WAYBEL24:21;

let a, b be object ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in *graph f1 or [a,b] in *graph f2 )

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

f2 is Function of X,S by WAYBEL24:21;

then A3: dom f2 = the carrier of X by FUNCT_2:def 1;

assume A4: [a,b] in *graph f1 ; :: thesis: [a,b] in *graph f2

then A5: ( a in dom f1 & b in f1 . a ) by WAYBEL26:38;

f1 is Function of X,S by WAYBEL24:21;

then A6: dom f1 = the carrier of X by FUNCT_2:def 1;

then reconsider a9 = a as Element of X by A4, WAYBEL26:38;

F1 . a9 is Element of S ;

then f1 . a in the carrier of (InclPoset the topology of Y) by A2;

then A7: f1 . a in the topology of Y by YELLOW_1:1;

F2 . a9 is Element of S ;

then f2 . a in the carrier of (InclPoset the topology of Y) by A2;

then A8: f2 . a in the topology of Y by YELLOW_1:1;

[(f1 . a9),(f2 . a9)] in the InternalRel of S by A1, WAYBEL24:20;

then [(f1 . a),(f2 . a)] in RelIncl the topology of Y by A2, YELLOW_1:1;

then f1 . a c= f2 . a by A7, A8, WELLORD2:def 1;

hence [a,b] in *graph f2 by A6, A3, A5, WAYBEL26:38; :: thesis: verum