let X be non empty monotone-convergence TopSpace; for N being eventually-directed net of Omega X holds sup N in Lim N
let N be eventually-directed net of Omega X; sup N in Lim N
rng (netmap (N,(Omega X))) is directed
by WAYBEL_2:18;
then reconsider D = rng the mapping of N as non empty directed Subset of (Omega X) ;
for V being a_neighborhood of sup N holds N is_eventually_in V
proof
let V be
a_neighborhood of
sup N;
N is_eventually_in V
A1:
Int V c= V
by TOPS_1:16;
A2:
TopStruct(# the
carrier of
X, the
topology of
X #)
= TopStruct(# the
carrier of
(Omega X), the
topology of
(Omega X) #)
by Def2;
then reconsider I =
Int V as
Subset of
X ;
A3:
I is
open
by A2, TOPS_3:76;
sup N in I
by CONNSP_2:def 1;
then
Sup in I
by WAYBEL_2:def 1;
then
D meets I
by A3, Def4;
then consider y being
object such that A4:
y in D
and A5:
y in I
by XBOOLE_0:3;
reconsider y =
y as
Point of
X by A5;
consider x being
object such that A6:
x in dom the
mapping of
N
and A7:
the
mapping of
N . x = y
by A4, FUNCT_1:def 3;
reconsider x =
x as
Element of
N by A6;
consider j being
Element of
N such that A8:
for
k being
Element of
N st
j <= k holds
N . x <= N . k
by WAYBEL_0:11;
take
j
;
WAYBEL_0:def 11 for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in V )
let k be
Element of
N;
( not j <= k or N . k in V )
assume
j <= k
;
N . k in V
then
N . x <= N . k
by A8;
then consider Y being
Subset of
X such that A9:
Y = {(N . k)}
and A10:
N . x in Cl Y
by Def2;
Y meets I
by A3, A5, A7, A10, PRE_TOPC:def 7;
then consider m being
object such that A11:
m in Y /\ I
by XBOOLE_0:4;
m in Y
by A11, XBOOLE_0:def 4;
then A12:
m = N . k
by A9, TARSKI:def 1;
m in I
by A11, XBOOLE_0:def 4;
hence
N . k in V
by A12, A1;
verum
end;
hence
sup N in Lim N
by YELLOW_6:def 15; verum