let Y be T_0-TopSpace; :: thesis: ( 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:] )

for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] ; :: thesis: InclPoset the topology of Y is continuous

S_{4}[Y]
_{5}[Y]
by Lm4;

then S_{6}[Y]
by Lm5;

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

for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] )

hereby :: thesis: ( ( 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:] ) implies InclPoset the topology of Y is continuous )

assume A1:
for X being non empty TopSpacefor f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] ) implies InclPoset the topology of Y is continuous )

assume
InclPoset the topology of Y is continuous
; :: thesis: 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:]

then S_{6}[Y]
by Lm8;

hence 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:] by Lm6; :: thesis: verum

end;for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:]

then S

hence 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:] by Lm6; :: thesis: verum

for f being continuous Function of X,(Sigma (InclPoset the topology of Y)) holds *graph f is open Subset of [:X,Y:] ; :: thesis: InclPoset the topology of Y is continuous

S

proof

then
S
let X be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: *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; :: thesis: verum

end;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; :: thesis: 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; :: thesis: *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; :: thesis: verum

then S

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