let X be monotone-convergence T_0-TopSpace; :: thesis: Omega X is up-complete
for A being non empty directed Subset of (Omega X) holds ex_sup_of A, Omega X by Def4;
hence Omega X is up-complete by WAYBEL_0:75; :: thesis: verum