for X being non empty monotone-convergence TopSpace
for N being eventually-directed prenet of Omega X holds ex_sup_of N