let Y be T_0-TopSpace; :: thesis: ( S_{6}[Y] implies S_{4}[Y] )

assume A1: S_{6}[Y]
; :: thesis: S_{4}[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;

assume A1: S

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:]

then reconsider A = *graph f as Subset of [:X,Y:] by TARSKI:def 3;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 A3, A4, WAYBEL26:38;

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 A2, YELLOW_1:1;

s2 in f . s1 by A3, A4, WAYBEL26:38;

then s in [: the carrier of X, the carrier of Y:] by A4, A5, A6, ZFMISC_1:87;

hence s in the carrier of [:X,Y:] by BORSUK_1:def 2; :: thesis: verum

end;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 A3, A4, WAYBEL26:38;

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 A2, YELLOW_1:1;

s2 in f . s1 by A3, A4, WAYBEL26:38;

then s in [: the carrier of X, the carrier of Y:] by A4, A5, A6, ZFMISC_1:87;

hence s in the carrier of [:X,Y:] by BORSUK_1:def 2; :: thesis: verum

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 )

hence
*graph f is open Subset of [:X,Y:]
by YELLOW_9:31; :: thesis: verumex 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 A7, A8, WAYBEL26:38;

A10: x in dom f by A7, A8, WAYBEL26:38;

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 A11, PRE_TOPC:def 2;

y in Int W by A9, TOPS_1:23;

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 A10, A12, CONNSP_2:def 1, FUNCT_1:def 7;

hence p in a by A8, ZFMISC_1:87; :: thesis: a c= A

thus a c= A :: thesis: verum

end;( 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 A7, A8, WAYBEL26:38;

A10: x in dom f by A7, A8, WAYBEL26:38;

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 A11, PRE_TOPC:def 2;

y in Int W by A9, TOPS_1:23;

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 A10, A12, CONNSP_2:def 1, FUNCT_1:def 7;

hence p in a by A8, ZFMISC_1:87; :: 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 A16, FUNCT_1:def 7;

s2 in V by A15, ZFMISC_1:87;

then s2 in f . s1 by A17, A14, SETFAM_1:def 1;

hence [s1,s2] in A by A18, WAYBEL26:38; :: thesis: verum

end;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 A16, FUNCT_1:def 7;

s2 in V by A15, ZFMISC_1:87;

then s2 in f . s1 by A17, A14, SETFAM_1:def 1;

hence [s1,s2] in A by A18, WAYBEL26:38; :: thesis: verum