let Y be T_0-TopSpace; ( 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:]
; InclPoset the topology of Y is continuous
S5[Y]
proof
let T be
Scott TopAugmentation of
InclPoset the
topology of
Y;
{ [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;
verum
end;
then
S6[Y]
by Lm5;
hence
InclPoset the topology of Y is continuous
by Lm7; verum