for X being non empty monotone-convergence TopSpace
for N being eventually-directed net of Omega X holds sup N in Lim N