let Y be T_0-TopSpace; :: thesis: ( InclPoset the topology of Y is continuous iff for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) )

thus ( InclPoset the topology of Y is continuous implies for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) ) by Lm8; :: thesis: ( ( for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) ) implies InclPoset the topology of Y is continuous )

assume A1: for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) ; :: thesis: InclPoset the topology of Y is continuous

S_{6}[Y]

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) )

thus ( InclPoset the topology of Y is continuous implies for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) ) by Lm8; :: thesis: ( ( for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) ) implies InclPoset the topology of Y is continuous )

assume A1: for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) ; :: thesis: InclPoset the topology of Y is continuous

S

proof

hence
InclPoset the topology of Y is continuous
by Lm7; :: thesis: verum
let T be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of T st

( V in H & meet H is a_neighborhood of y )

let y be Element of Y; :: thesis: for V being open a_neighborhood of y ex H being open Subset of T 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 T st

( V in H & meet H is a_neighborhood of y )

consider H being open Subset of (Sigma (InclPoset the topology of Y)) such that

A2: ( V in H & meet H is a_neighborhood of y ) by A1;

( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def 4;

then reconsider G = H as Subset of T ;

the topology of T = the topology of (Sigma (InclPoset the topology of Y)) by Th13;

then G in the topology of T by PRE_TOPC:def 2;

then H is open Subset of T by PRE_TOPC:def 2;

hence ex H being open Subset of T st

( V in H & meet H is a_neighborhood of y ) by A2; :: thesis: verum

end;for V being open a_neighborhood of y ex H being open Subset of T st

( V in H & meet H is a_neighborhood of y )

let y be Element of Y; :: thesis: for V being open a_neighborhood of y ex H being open Subset of T 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 T st

( V in H & meet H is a_neighborhood of y )

consider H being open Subset of (Sigma (InclPoset the topology of Y)) such that

A2: ( V in H & meet H is a_neighborhood of y ) by A1;

( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def 4;

then reconsider G = H as Subset of T ;

the topology of T = the topology of (Sigma (InclPoset the topology of Y)) by Th13;

then G in the topology of T by PRE_TOPC:def 2;

then H is open Subset of T by PRE_TOPC:def 2;

hence ex H being open Subset of T st

( V in H & meet H is a_neighborhood of y ) by A2; :: thesis: verum