let X, Y be non empty TopSpace; :: thesis: for S being Scott TopAugmentation of InclPoset the topology of Y
for W being open Subset of [:X,Y:] holds W,the carrier of X *graph is continuous Function of X,S
let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for W being open Subset of [:X,Y:] holds W,the carrier of X *graph is continuous Function of X,S
let W be open Subset of [:X,Y:]; :: thesis: W,the carrier of X *graph is continuous Function of X,S
set f = W,the carrier of X *graph ;
the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by BORSUK_1:def 5;
then reconsider W = W as Relation of the carrier of X,the carrier of Y ;
A1: dom W c= the carrier of X ;
A2: dom (W,the carrier of X *graph ) = the carrier of X by Def5;
A3: the carrier of (InclPoset the topology of Y) = the topology of Y by YELLOW_1:1;
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;
rng (W,the carrier of X *graph ) c= the carrier of S

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (W,the carrier of X *graph ) or y in the carrier of S )
assume y in rng (W,the carrier of X *graph ) ; :: thesis: y in the carrier of S
then consider x being set such that
A5: ( x in dom (W,the carrier of X *graph ) & y = (W,the carrier of X *graph ) . x ) by FUNCT_1:def 5;
reconsider x = x as Element of X by A5, Def5;
y = Im W,x by A5, Def5;
then y is open Subset of Y by Th43;
hence y in the carrier of S by A3, A4, PRE_TOPC:def 5; :: thesis: verum

end;

then reconsider f = W,the carrier of X *graph as Function of X,S by A2, FUNCT_2:4;
*graph f = W by A1, Th42;
hence W,the carrier of X *graph is continuous Function of X,S by Th41; :: thesis: verum