let Y be T_0-TopSpace; :: thesis: ( S_{3}[Y] implies S_{4}[Y] )

assume A1: S_{3}[Y]
; :: thesis: S_{4}[Y]

set S = Sigma (InclPoset the topology of Y);

let X be non empty TopSpace; :: thesis: for T being Scott TopAugmentation of InclPoset the topology of Y

for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]

let T be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]

A2: the topology of T = sigma (InclPoset the topology of Y) by YELLOW_9:51;

let f be continuous Function of X,T; :: thesis: *graph f is open Subset of [:X,Y:]

( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def 4;

then A3: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) & TopRelStr(# the carrier of T, the InternalRel of T, the topology of T #) = TopRelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) by A2, YELLOW_9:51;

then reconsider F = Theta (X,Y) as Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,T)) by Th10;

ContMaps (X,T) = ContMaps (X,(Sigma (InclPoset the topology of Y))) by A3, Th10;

then F is isomorphic by A1;

then ( f in the carrier of (ContMaps (X,T)) & rng F = the carrier of (ContMaps (X,T)) ) by WAYBEL24:def 3, WAYBEL_0:66;

then consider W being object such that

A4: W in dom F and

A5: f = F . W by FUNCT_1:def 3;

dom F = the carrier of (InclPoset the topology of [:X,Y:]) by FUNCT_2:def 1

.= the topology of [:X,Y:] by YELLOW_1:1 ;

then reconsider W = W as open Subset of [:X,Y:] by A4, PRE_TOPC:def 2;

reconsider R = W as Relation of the carrier of X, the carrier of Y by BORSUK_1:def 2;

A6: dom R c= the carrier of X ;

f = (W, the carrier of X) *graph by A5, Def3;

hence *graph f is open Subset of [:X,Y:] by A6, WAYBEL26:41; :: thesis: verum

assume A1: S

set S = Sigma (InclPoset the topology of Y);

let X be non empty TopSpace; :: thesis: for T being Scott TopAugmentation of InclPoset the topology of Y

for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]

let T be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]

A2: the topology of T = sigma (InclPoset the topology of Y) by YELLOW_9:51;

let f be continuous Function of X,T; :: thesis: *graph f is open Subset of [:X,Y:]

( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def 4;

then A3: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) & TopRelStr(# the carrier of T, the InternalRel of T, the topology of T #) = TopRelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) by A2, YELLOW_9:51;

then reconsider F = Theta (X,Y) as Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,T)) by Th10;

ContMaps (X,T) = ContMaps (X,(Sigma (InclPoset the topology of Y))) by A3, Th10;

then F is isomorphic by A1;

then ( f in the carrier of (ContMaps (X,T)) & rng F = the carrier of (ContMaps (X,T)) ) by WAYBEL24:def 3, WAYBEL_0:66;

then consider W being object such that

A4: W in dom F and

A5: f = F . W by FUNCT_1:def 3;

dom F = the carrier of (InclPoset the topology of [:X,Y:]) by FUNCT_2:def 1

.= the topology of [:X,Y:] by YELLOW_1:1 ;

then reconsider W = W as open Subset of [:X,Y:] by A4, PRE_TOPC:def 2;

reconsider R = W as Relation of the carrier of X, the carrier of Y by BORSUK_1:def 2;

A6: dom R c= the carrier of X ;

f = (W, the carrier of X) *graph by A5, Def3;

hence *graph f is open Subset of [:X,Y:] by A6, WAYBEL26:41; :: thesis: verum