let Y be T_0-TopSpace; :: thesis: ( S3[Y] implies S4[Y] )
assume A1: S3[Y] ; :: thesis: S4[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 ;
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 ;
then F is isomorphic by A1;
then ( f in the carrier of (ContMaps (X,T)) & rng F = the carrier of (ContMaps (X,T)) ) by ;
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 ;
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 ;
hence *graph f is open Subset of [:X,Y:] by ; :: thesis: verum