let X be non empty TopSpace; :: thesis: ( ( for N being eventually-directed net of Omega X holds
( ex_sup_of N & sup N in Lim N ) ) implies X is monotone-convergence )
assume A1: for N being eventually-directed net of Omega X holds
( ex_sup_of N & sup N in Lim N ) ; :: thesis: X is monotone-convergence
let D be non empty directed Subset of (Omega X); :: according to WAYBEL25:def 4 :: thesis: ( ex_sup_of D, Omega X & ( for V being open Subset of X st sup D in V holds
D meets V ) )
Net-Str D = NetStr(# D,( the InternalRel of (Omega X) |_2 D),((id the carrier of (Omega X)) | D) #) by WAYBEL17:def 4;
then A2: rng the mapping of (Net-Str D) = D by YELLOW14:2;
ex_sup_of Net-Str D by A1;
hence ex_sup_of D, Omega X by A2; :: thesis: for V being open Subset of X st sup D in V holds
D meets V
let V be open Subset of X; :: thesis: ( sup D in V implies D meets V )
assume A3: sup D in V ; :: thesis: D meets V
reconsider Z = V as Subset of (Omega X) by Lm1;
A4: sup (Net-Str D) = Sup by WAYBEL_2:def 1
.= sup (rng the mapping of (Net-Str D)) ;
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) by Def2;
then Int Z = Int V by TOPS_3:77;
then sup (Net-Str D) in Int Z by A2, A3, A4, TOPS_1:23;
then A5: Z is a_neighborhood of sup (Net-Str D) by CONNSP_2:def 1;
sup (Net-Str D) in Lim (Net-Str D) by A1;
then Net-Str D is_eventually_in V by A5, YELLOW_6:def 15;
then consider i being Element of (Net-Str D) such that
A6: for j being Element of (Net-Str D) st i <= j holds
(Net-Str D) . j in V ;
now :: thesis: ex a being Element of the carrier of (Omega X) st
( a in D & a in V )
take a = (Net-Str D) . i; :: thesis: ( a in D & a in V )
dom the mapping of (Net-Str D) = the carrier of (Net-Str D) by FUNCT_2:def 1;
hence a in D by A2, FUNCT_1:def 3; :: thesis: a in V
thus a in V by A6; :: thesis: verum
end;
hence D meets V by XBOOLE_0:3; :: thesis: verum