theorem Th41: :: YELLOW_6:41

for T being non empty 1-sorted
for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C) holds
( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S )