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 ;

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

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; :: thesis: verum

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 ;

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

proof

then reconsider f = (W, the carrier of X) *graph as Function of X,S by A1, FUNCT_2:2;
let y be object ; :: 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 object such that

A3: x in dom ((W, the carrier of X) *graph) and

A4: y = ((W, the carrier of X) *graph) . x by FUNCT_1:def 3;

reconsider x = x as Element of X by A3, Def5;

y = Im (W,x) by A4, Def5;

then y is open Subset of Y by Th42;

hence y in the carrier of S by A2, PRE_TOPC:def 2; :: thesis: verum

end;assume y in rng ((W, the carrier of X) *graph) ; :: thesis: y in the carrier of S

then consider x being object such that

A3: x in dom ((W, the carrier of X) *graph) and

A4: y = ((W, the carrier of X) *graph) . x by FUNCT_1:def 3;

reconsider x = x as Element of X by A3, Def5;

y = Im (W,x) by A4, Def5;

then y is open Subset of Y by Th42;

hence y in the carrier of S by A2, PRE_TOPC:def 2; :: thesis: verum

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; :: thesis: verum