theorem Th31: :: WAYBEL25:31

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