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