let T be T_0-TopSpace; :: thesis: ( InclPoset the topology of T is continuous implies S_{6}[T] )

assume A1: InclPoset the topology of T is continuous ; :: thesis: S_{6}[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)

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

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

assume A1: InclPoset the topology of T is continuous ; :: thesis: S

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

reconsider H = wayabove Z1 as open Subset of S by A1, WAYBEL11:36;
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)

end;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

hence
s in meet (uparrow Z)
by SETFAM_1:def 1; :: thesis: verums 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;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

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

then reconsider mH = meet H as Subset of T ;
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;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

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