let T be T_0-TopSpace; :: thesis: ( T is trivial implies T is monotone-convergence )
assume T is trivial ; :: thesis: T is monotone-convergence
then consider d being Element of T such that
A1: the carrier of T = {d} by TEX_1:def 1;
reconsider d = d as Element of (Omega T) by Lm1;
let D be non empty directed Subset of (Omega T); :: according to WAYBEL25:def 4 :: thesis: ( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) )
A2: the carrier of T = the carrier of (Omega T) by Lm1;
then D = {d} by A1, Lm7;
hence ex_sup_of D, Omega T by YELLOW_0:38; :: thesis: for V being open Subset of T st sup D in V holds
D meets V
let V be open Subset of T; :: thesis: ( sup D in V implies D meets V )
A3: {d} meets {d} ;
assume sup D in V ; :: thesis: D meets V
then V = {d} by A1, Lm7;
hence D meets V by A1, A2, A3, Lm7; :: thesis: verum