let X be non empty monotone-convergence TopSpace; :: thesis: for N being eventually-directed prenet of Omega X holds ex_sup_of N
let N be eventually-directed prenet of Omega X; :: thesis: ex_sup_of N
rng (netmap (N,(Omega X))) is directed by WAYBEL_2:18;
hence ex_sup_of rng the mapping of N, Omega X by Def4; :: according to WAYBEL_9:def 3 :: thesis: verum