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

assume A1: S_{5}[Y]
; :: thesis: S_{6}[Y]

let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of S st

( V in H & meet H is a_neighborhood of y )

reconsider A = { [W,z] where W is open Subset of Y, z is Element of Y : z in W } as open Subset of [:S,Y:] by A1;

let y be Element of Y; :: thesis: for V being open a_neighborhood of y ex H being open Subset of S st

( V in H & meet H is a_neighborhood of y )

let V be open a_neighborhood of y; :: thesis: ex H being open Subset of S st

( V in H & meet H is a_neighborhood of y )

( the topology of S is Basis of S & the topology of Y is Basis of Y ) by CANTOR_1:2;

then reconsider B = { [:a,b:] where a is Subset of S, b is Subset of Y : ( a in the topology of S & b in the topology of Y ) } as Basis of [:S,Y:] by YELLOW_9:40;

y in V by CONNSP_2:4;

then [V,y] in A ;

then consider ab being Subset of [:S,Y:] such that

A2: ab in B and

A3: [V,y] in ab and

A4: ab c= A by YELLOW_9:31;

consider H being Subset of S, W being Subset of Y such that

A5: ab = [:H,W:] and

A6: H in the topology of S and

A7: W in the topology of Y by A2;

reconsider H = H as open Subset of S by A6, PRE_TOPC:def 2;

A8: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;

meet H c= the carrier of Y

reconsider W = W as open Subset of Y by A7, PRE_TOPC:def 2;

W c= mH

take H ; :: thesis: ( V in H & meet H is a_neighborhood of y )

thus V in H by A3, A5, ZFMISC_1:87; :: thesis: meet H is a_neighborhood of y

y in W by A3, A5, ZFMISC_1:87;

hence meet H is a_neighborhood of y by A15, CONNSP_2:def 1; :: thesis: verum

assume A1: S

let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of S st

( V in H & meet H is a_neighborhood of y )

reconsider A = { [W,z] where W is open Subset of Y, z is Element of Y : z in W } as open Subset of [:S,Y:] by A1;

let y be Element of Y; :: thesis: for V being open a_neighborhood of y ex H being open Subset of S st

( V in H & meet H is a_neighborhood of y )

let V be open a_neighborhood of y; :: thesis: ex H being open Subset of S st

( V in H & meet H is a_neighborhood of y )

( the topology of S is Basis of S & the topology of Y is Basis of Y ) by CANTOR_1:2;

then reconsider B = { [:a,b:] where a is Subset of S, b is Subset of Y : ( a in the topology of S & b in the topology of Y ) } as Basis of [:S,Y:] by YELLOW_9:40;

y in V by CONNSP_2:4;

then [V,y] in A ;

then consider ab being Subset of [:S,Y:] such that

A2: ab in B and

A3: [V,y] in ab and

A4: ab c= A by YELLOW_9:31;

consider H being Subset of S, W being Subset of Y such that

A5: ab = [:H,W:] and

A6: H in the topology of S and

A7: W in the topology of Y by A2;

reconsider H = H as open Subset of S by A6, PRE_TOPC:def 2;

A8: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;

meet H c= the carrier of Y

proof

then reconsider mH = meet H as Subset of Y ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet H or x in the carrier of Y )

H <> {} by A3, A5;

then consider A being object such that

A9: A in H by XBOOLE_0:def 1;

A in the carrier of S by A9;

then A10: A in the topology of Y by A8, YELLOW_1:1;

reconsider A = A as set by TARSKI:1;

assume x in meet H ; :: thesis: x in the carrier of Y

then x in A by A9, SETFAM_1:def 1;

hence x in the carrier of Y by A10; :: thesis: verum

end;H <> {} by A3, A5;

then consider A being object such that

A9: A in H by XBOOLE_0:def 1;

A in the carrier of S by A9;

then A10: A in the topology of Y by A8, YELLOW_1:1;

reconsider A = A as set by TARSKI:1;

assume x in meet H ; :: thesis: x in the carrier of Y

then x in A by A9, SETFAM_1:def 1;

hence x in the carrier of Y by A10; :: thesis: verum

reconsider W = W as open Subset of Y by A7, PRE_TOPC:def 2;

W c= mH

proof

then A15:
W c= Int mH
by TOPS_1:24;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in W or w in mH )

assume A11: w in W ; :: thesis: w in mH

hence w in mH by A12, SETFAM_1:def 1; :: thesis: verum

end;assume A11: w in W ; :: thesis: w in mH

A12: now :: thesis: for a being set st a in H holds

w in a

H <> {}
by A3, A5;w in a

let a be set ; :: thesis: ( a in H implies w in a )

assume a in H ; :: thesis: w in a

then [a,w] in ab by A5, A11, ZFMISC_1:87;

then [a,w] in A by A4;

then consider a1 being open Subset of Y, w1 being Element of Y such that

A13: [a,w] = [a1,w1] and

A14: w1 in a1 ;

a = a1 by A13, XTUPLE_0:1;

hence w in a by A13, A14, XTUPLE_0:1; :: thesis: verum

end;assume a in H ; :: thesis: w in a

then [a,w] in ab by A5, A11, ZFMISC_1:87;

then [a,w] in A by A4;

then consider a1 being open Subset of Y, w1 being Element of Y such that

A13: [a,w] = [a1,w1] and

A14: w1 in a1 ;

a = a1 by A13, XTUPLE_0:1;

hence w in a by A13, A14, XTUPLE_0:1; :: thesis: verum

hence w in mH by A12, SETFAM_1:def 1; :: thesis: verum

take H ; :: thesis: ( V in H & meet H is a_neighborhood of y )

thus V in H by A3, A5, ZFMISC_1:87; :: thesis: meet H is a_neighborhood of y

y in W by A3, A5, ZFMISC_1:87;

hence meet H is a_neighborhood of y by A15, CONNSP_2:def 1; :: thesis: verum