let Y be T_0-TopSpace; ( S3[Y] implies S4[Y] )
assume A1:
S3[Y]
; S4[Y]
set S = Sigma (InclPoset the topology of Y);
let X be non empty TopSpace; 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; 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; *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; verum