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 CONNSP_2:def 1, TOPS_1:16;
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 (waybelow W) by A1, WAYBEL_3:def 5
.= union (waybelow W) by YELLOW_1:22 ;
then consider Z being set such that
A3: y in Z and
A4: Z in waybelow W by A2, TARSKI:def 4;
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 (uparrow Z)
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in Z or s in meet (uparrow Z) )
assume A7: s in Z ; :: thesis: s in meet (uparrow Z)
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 A8, WAYBEL_0:18;
then Z c= z by YELLOW_1:3;
hence s in z by A7; :: thesis: verum
end;
hence s in meet (uparrow Z) by SETFAM_1:def 1; :: thesis: verum
end;
reconsider H = wayabove Z1 as open Subset of S by A1, WAYBEL11:36;
take H ; :: thesis: ( V in H & meet H is a_neighborhood of y )
Z << W by A4, WAYBEL_3:7;
then A9: V in wayabove Z ;
hence A10: V in H by A5, YELLOW12:13; :: 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 A10, SETFAM_1:def 1;
hence s in the carrier of T ; :: thesis: verum
end;
then reconsider mH = meet H as Subset of T ;
meet (uparrow Z) c= meet (wayabove Z) by A9, SETFAM_1:6, WAYBEL_3:11;
then meet (uparrow Z) c= meet (wayabove Z1) by A5, YELLOW12:13;
then Z2 c= mH by A6;
then Z2 c= Int mH by TOPS_1:24;
hence meet H is a_neighborhood of y by A3, CONNSP_2:def 1; :: thesis: verum