let X be non empty monotone-convergence TopSpace; :: thesis: for N being eventually-directed net of Omega X holds N is convergent
let N be eventually-directed net of Omega X; :: thesis: N is convergent
thus Lim N <> {} by Th32; :: according to YELLOW_6:def 16 :: thesis: verum