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 ) )