let Y be T_0-TopSpace; :: thesis: ( S₃[Y] implies S₄[Y] )
assume A1: S₃[Y] ; :: thesis: S₄[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:]
set S = Sigma (InclPoset the topology of 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:]
( 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 & the topology of T = sigma (InclPoset the topology of Y) & the topology of (Sigma (InclPoset the topology of Y)) = sigma (InclPoset the topology of Y) ) by YELLOW_9:51, YELLOW_9:def 4;
then ( 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)) #) ) ;
then A2: ContMaps X,T = ContMaps X,(Sigma (InclPoset the topology of Y)) by Th13;
then reconsider F = Theta X,Y as Function of (InclPoset the topology of [:X,Y:]),(ContMaps X,T) ;
A3: F is isomorphic by A1, A2;
let f be continuous Function of X,T; :: thesis: *graph f is open Subset of [:X,Y:]
A4: f in the carrier of (ContMaps X,T) by WAYBEL24:def 3;
rng F = the carrier of (ContMaps X,T) by A3, WAYBEL_0:66;
then consider W being set such that
A5: ( W in dom F & f = F . W ) by A4, FUNCT_1:def 5;
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 A5, PRE_TOPC:def 5;
the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by BORSUK_1:def 5;
then reconsider R = W as Relation of the carrier of X,the carrier of Y ;
( f = W,the carrier of X *graph & dom R c= the carrier of X ) by A5, Def3;
hence *graph f is open Subset of [:X,Y:] by WAYBEL26:42; :: thesis: verum