let X, Y be non empty TopSpace; 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; 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:]; (W, the carrier of X) *graph is continuous Function of X,S
set f = (W, the carrier of X) *graph ;
reconsider W = W as Relation of the carrier of X, the carrier of Y by BORSUK_1:def 2;
A1:
dom ((W, the carrier of X) *graph) = the carrier of X
by Def5;
A2:
( the carrier of (InclPoset the topology of Y) = the topology of Y & 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_1:1, YELLOW_9:def 4;
rng ((W, the carrier of X) *graph) c= the carrier of S
then reconsider f = (W, the carrier of X) *graph as Function of X,S by A1, FUNCT_2:2;
dom W c= the carrier of X
;
then
*graph f = W
by Th41;
hence
(W, the carrier of X) *graph is continuous Function of X,S
by Th40; verum