theorem
:: WAYBEL29:26
for
Y
being
T_0-TopSpace
holds
(
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
:]
)