let Y be T_0-TopSpace; :: thesis: ( S₃[Y] implies S₄[Y] )
assume A1: S₃[Y] ; :: thesis: S₄[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