let Y be T_0-TopSpace; :: thesis:
assume A1: S₅[Y] ; :: thesis:
let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis:
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:
let V be open a_neighborhood of y; :: thesis:
( 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:6;
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 5;
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

let x be set ; :: according to TARSKI:def 3 :: thesis:
H <> {} by A3, A5;
then consider A being set 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;
assume x in meet H ; :: thesis:
then x in A by A9, SETFAM_1:def 1;
hence x in the carrier of Y by A10; :: thesis:

end;

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

let w be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: w in W ; :: thesis:

A12: now

let a be set ; :: thesis:
assume a in H ; :: thesis:
then [a,w] in ab by A5, A11, ZFMISC_1:106;
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, ZFMISC_1:33;
hence w in a by A13, A14, ZFMISC_1:33; :: thesis:

end;

end;