let Y be T_0-TopSpace; :: thesis: ( S5[Y] implies S6[Y] )
assume A1: S5[Y] ; :: thesis: S6[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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
hence w in a by ; :: thesis: verum
end;
H <> {} by A3, A5;
hence w in mH by ; :: 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 ; :: thesis: meet H is a_neighborhood of y
y in W by ;
hence meet H is a_neighborhood of y by ; :: thesis: verum