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

hereby :: thesis: ( { [W,y] where W is open Subset of , y is Element of : y in W } is open Subset of implies 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 is Element of : y in W } is open Subset of
then S₆[Y] by Lm8;
then S₄[Y] by Lm6;
hence { [W,y] where W is open Subset of , y is Element of : y in W } is open Subset of by Lm4; :: thesis: verum

end;

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

proof

let T be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: { [W,y] where W is open Subset of , y is Element of : y in W } is open Subset of
( 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 Th17;
then [:T,Y:] = [:(Sigma (InclPoset the topology of Y)),Y:] by Th10;
hence { [W,y] where W is open Subset of , y is Element of : y in W } is open Subset of by A1; :: thesis: verum

end;

then S₆[Y] by Lm5;
hence InclPoset the topology of Y is continuous by Lm7; :: thesis: verum