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