let T be T_0-TopSpace; :: thesis: ( InclPoset the topology of T is continuous implies S₆[T] )
assume A1: InclPoset the topology of T is continuous ; :: thesis: S₆[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: 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;
V in the topology of T by PRE_TOPC:def 5;
then reconsider W = V as Element of (InclPoset the topology of T) by YELLOW_1:1;
InclPoset the topology of T is satisfying_axiom_of_approximation by A1;
then A3: W = sup (waybelow W) by WAYBEL_3:def 5
.= union (waybelow W) by YELLOW_1:22 ;
A4: Int V c= V by TOPS_1:44;
y in Int V by CONNSP_2:def 1;
then consider Z being set such that
A5: ( y in Z & Z in waybelow W ) by A3, A4, TARSKI:def 4;
reconsider Z = Z as Element of (InclPoset the topology of T) by A5;
reconsider Z1 = Z as Element of S by A2;
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 5;
S is continuous by A1;
then reconsider H = wayabove Z1 as open Subset of S by WAYBEL11:36;
take H ; :: thesis: ( V in H & meet H is a_neighborhood of y )
Z << W by A5, WAYBEL_3:7;
then A6: V in wayabove Z ;
hence A7: V in H by A2, YELLOW12:13; :: thesis: meet H is a_neighborhood of y
meet H c= the carrier of T

proof

let s be set ; :: 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 A7, SETFAM_1:def 1;
hence s in the carrier of T ; :: thesis: verum

end;

then reconsider mH = meet H as Subset of T ;
wayabove Z c= uparrow Z by WAYBEL_3:11;
then meet (uparrow Z) c= meet (wayabove Z) by A6, SETFAM_1:7;
then A8: meet (uparrow Z) c= meet (wayabove Z1) by A2, YELLOW12:13;
Z c= meet (uparrow Z)

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in Z or s in meet (uparrow Z) )
assume A9: s in Z ; :: thesis: s in meet (uparrow Z)

now

let z be set ; :: thesis: ( z in uparrow Z implies s in z )
assume A10: z in uparrow Z ; :: thesis: s in z
then reconsider z1 = z as Element of (InclPoset the topology of T) ;
Z <= z1 by A10, WAYBEL_0:18;
then Z c= z by YELLOW_1:3;
hence s in z by A9; :: thesis: verum

end;

hence s in meet (uparrow Z) by SETFAM_1:def 1; :: thesis: verum

end;

then Z2 c= mH by A8, XBOOLE_1:1;
then Z2 c= Int mH by TOPS_1:56;
hence meet H is a_neighborhood of y by A5, CONNSP_2:def 1; :: thesis: verum