:: deftheorem Def4 defines monotone-convergence WAYBEL25:def 4 :
for T being non empty TopSpace holds
( T is monotone-convergence iff for D being non empty directed Subset of (Omega T) holds
( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) ) );