for X being non empty TopSpace st ( for N being eventually-directed net of Omega X holds
( ex_sup_of N & sup N in Lim N ) ) holds
X is monotone-convergence