let T be T_0-TopSpace; :: thesis: ( InclPoset the topology of T is continuous implies S6[T] )
assume A1: InclPoset the topology of T is continuous ; :: thesis: S6[T]
let S be Scott TopAugmentation of InclPoset the topology of T; :: thesis: for y being Element of T
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 y be Element of T; :: 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 )

A2: ( Int V c= V & y in Int V ) by ;
V in the topology of T by PRE_TOPC:def 2;
then reconsider W = V as Element of (InclPoset the topology of T) by YELLOW_1:1;
W = sup () by
.= union () by YELLOW_1:22 ;
then consider Z being set such that
A3: y in Z and
A4: Z in waybelow W by ;
reconsider Z = Z as Element of (InclPoset the topology of T) by A4;
A5: RelStr(# the carrier of (InclPoset the topology of T), the InternalRel of (InclPoset the topology of T) #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
then reconsider Z1 = Z as Element of S ;
Z in the carrier of (InclPoset the topology of T) ;
then Z in the topology of T by YELLOW_1:1;
then reconsider Z2 = Z as open Subset of T by PRE_TOPC:def 2;
A6: Z c= meet ()
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in Z or s in meet () )
assume A7: s in Z ; :: thesis: s in meet ()
now :: thesis: for z being set st z in uparrow Z holds
s in z
let z be set ; :: thesis: ( z in uparrow Z implies s in z )
assume A8: z in uparrow Z ; :: thesis: s in z
then reconsider z1 = z as Element of (InclPoset the topology of T) ;
Z <= z1 by ;
then Z c= z by YELLOW_1:3;
hence s in z by A7; :: thesis: verum
end;
hence s in meet () by SETFAM_1:def 1; :: thesis: verum
end;
reconsider H = wayabove Z1 as open Subset of S by ;
take H ; :: thesis: ( V in H & meet H is a_neighborhood of y )
Z << W by ;
then A9: V in wayabove Z ;
hence A10: V in H by ; :: thesis: meet H is a_neighborhood of y
meet H c= the carrier of T
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in meet H or s in the carrier of T )
assume s in meet H ; :: thesis: s in the carrier of T
then s in V by ;
hence s in the carrier of T ; :: thesis: verum
end;
then reconsider mH = meet H as Subset of T ;
meet () c= meet () by ;
then meet () c= meet (wayabove Z1) by ;
then Z2 c= mH by A6;
then Z2 c= Int mH by TOPS_1:24;
hence meet H is a_neighborhood of y by ; :: thesis: verum