let Y be T_0-TopSpace; ( InclPoset the topology of Y is continuous iff for X being non empty TopSpace
for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] )
assume A1:
for X being non empty TopSpace
for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:]
; InclPoset the topology of Y is continuous
S4[Y]
proof
let X be non
empty TopSpace;
for T being Scott TopAugmentation of InclPoset the topology of Y
for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]let T be
Scott TopAugmentation of
InclPoset the
topology of
Y;
for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]let f be
continuous Function of
X,
T;
*graph f is open Subset of [:X,Y:]
A2:
(
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 =
f as
Function of
X,
(Sigma (InclPoset the topology of Y)) ;
(
TopStruct(# the
carrier of
X, the
topology of
X #)
= TopStruct(# the
carrier of
X, the
topology of
X #) &
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 A2, Th13;
then
g is
continuous
by YELLOW12:36;
hence
*graph f is
open Subset of
[:X,Y:]
by A1;
verum
end;
then
S5[Y]
by Lm4;
then
S6[Y]
by Lm5;
hence
InclPoset the topology of Y is continuous
by Lm7; verum