let Y be T_0-TopSpace; :: thesis: ( InclPoset the topology of Y is continuous iff { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] )

S_{5}[Y]
_{6}[Y]
by Lm5;

hence InclPoset the topology of Y is continuous by Lm7; :: thesis: verum

hereby :: thesis: ( { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] implies InclPoset the topology of Y is continuous )

assume A1:
{ [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:]
; :: thesis: InclPoset the topology of Y is continuous assume
InclPoset the topology of Y is continuous
; :: thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:]

then S_{6}[Y]
by Lm8;

then S_{4}[Y]
by Lm6;

hence { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] by Lm4; :: thesis: verum

end;then S

then S

hence { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:(Sigma (InclPoset the topology of Y)),Y:] by Lm4; :: thesis: verum

S

proof

then
S
let T be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:T,Y:]

( 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 ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y, the topology of Y #) & TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) by Th13;

then [:T,Y:] = [:(Sigma (InclPoset the topology of Y)),Y:] by Th7;

hence { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:T,Y:] by A1; :: thesis: verum

end;( 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 ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y, the topology of Y #) & TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) by Th13;

then [:T,Y:] = [:(Sigma (InclPoset the topology of Y)),Y:] by Th7;

hence { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:T,Y:] by A1; :: thesis: verum

hence InclPoset the topology of Y is continuous by Lm7; :: thesis: verum