theorem :: WAYBEL29:28

for Y being T_0-TopSpace holds

( InclPoset the topology of Y is continuous iff for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) )

( InclPoset the topology of Y is continuous iff for y being Element of Y

for V being open a_neighborhood of y ex H being open Subset of (Sigma (InclPoset the topology of Y)) st

( V in H & meet H is a_neighborhood of y ) )