let Y be T_0-TopSpace; :: thesis: ( S6[Y] implies S4[Y] )
assume A1: S6[Y] ; :: thesis: S4[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:]
let f be continuous Function of X,T; :: thesis: *graph f is open Subset of [:X,Y:]
( the topology of X is Basis of X & the topology of Y is Basis of Y ) by CANTOR_1:2;
then reconsider B = { [:a,b:] where a is Subset of X, b is Subset of Y : ( a in the topology of X & b in the topology of Y ) } as Basis of [:X,Y:] by YELLOW_9:40;
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;
now :: thesis: for s being object st s in *graph f holds
s in the carrier of [:X,Y:]
let s be object ; :: thesis: ( s in *graph f implies s in the carrier of [:X,Y:] )
assume A3: s in *graph f ; :: thesis: s in the carrier of [:X,Y:]
then consider s1, s2 being object such that
A4: s = [s1,s2] by RELAT_1:def 1;
A5: s1 in dom f by ;
then f . s1 in rng f by FUNCT_1:def 3;
then f . s1 in the carrier of T ;
then A6: f . s1 in the topology of Y by ;
s2 in f . s1 by ;
then s in [: the carrier of X, the carrier of Y:] by ;
hence s in the carrier of [:X,Y:] by BORSUK_1:def 2; :: thesis: verum
end;
then reconsider A = *graph f as Subset of [:X,Y:] by TARSKI:def 3;
now :: thesis: for p being Point of [:X,Y:] st p in A holds
ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A )
let p be Point of [:X,Y:]; :: thesis: ( p in A implies ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A ) )

assume A7: p in A ; :: thesis: ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A )

then consider x, y being object such that
A8: p = [x,y] by RELAT_1:def 1;
A9: y in f . x by ;
A10: x in dom f by ;
then reconsider x = x as Element of X ;
f . x in the carrier of (InclPoset the topology of Y) by A2;
then A11: f . x in the topology of Y by YELLOW_1:1;
then reconsider y = y as Element of Y by A9;
reconsider W = f . x as open Subset of Y by ;
y in Int W by ;
then reconsider W = W as open a_neighborhood of y by CONNSP_2:def 1;
consider H being open Subset of T such that
A12: W in H and
A13: meet H is a_neighborhood of y by A1;
[#] T <> {} ;
then reconsider fH = f " H as open Subset of X by TOPS_2:43;
reconsider mH = meet H as a_neighborhood of y by A13;
Int (Int mH) = Int mH ;
then reconsider V = Int mH as open a_neighborhood of y by CONNSP_2:def 1;
reconsider a = [:fH,V:] as Subset of [:X,Y:] ;
take a = a; :: thesis: ( a in B & p in a & a c= A )
( V in the topology of Y & fH in the topology of X ) by PRE_TOPC:def 2;
hence a in B ; :: thesis: ( p in a & a c= A )
( y in Int mH & x in fH ) by ;
hence p in a by ; :: thesis: a c= A
thus a c= A :: thesis: verum
proof
let s1, s2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [s1,s2] in a or [s1,s2] in A )
A14: V c= mH by TOPS_1:16;
assume A15: [s1,s2] in a ; :: thesis: [s1,s2] in A
then A16: s1 in fH by ZFMISC_1:87;
then A17: f . s1 in H by FUNCT_1:def 7;
A18: s1 in dom f by ;
s2 in V by ;
then s2 in f . s1 by ;
hence [s1,s2] in A by ; :: thesis: verum
end;
end;
hence *graph f is open Subset of [:X,Y:] by YELLOW_9:31; :: thesis: verum