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:] )
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
S5[Y]
proof
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 & the
topology of
T = the
topology of
(Sigma (InclPoset the topology of Y)) )
by Th17, 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)) #) )
;
then
[:T,Y:] = [:(Sigma (InclPoset the topology of Y)),Y:]
by Th10;
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;
then
S6[Y]
by Lm5;
hence
InclPoset the topology of Y is continuous
by Lm7; :: thesis: verum