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

proof

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;

then reconsider mH = meet H as Subset of Y ;
reconsider W = W as open Subset of Y by A7, PRE_TOPC:def 2;
W c= mH

proof

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

A12: now :: thesis: for a being set st a in H holds
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;

H <> {} by A3, A5;
hence w in mH by A12, SETFAM_1:def 1; :: thesis: verum

end;

then A15: W c= Int mH by TOPS_1:24;
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