let X be non empty monotone-convergence TopSpace; :: thesis: for N being eventually-directed net of Omega X holds sup N in Lim N
let N be eventually-directed net of Omega X; :: thesis: 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;
:: thesis: N is_eventually_in V
A1:
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 ;
A2:
I is
open
by A1, 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 A2, Def4;
then consider y being
set such that A3:
y in D
and A4:
y in I
by XBOOLE_0:3;
reconsider y =
y as
Point of
X by A4;
consider x being
set such that A5:
x in dom the
mapping of
N
and A6:
the
mapping of
N . x = y
by A3, FUNCT_1:def 5;
reconsider x =
x as
Element of
N by A5;
consider j being
Element of
N such that A7:
for
k being
Element of
N st
j <= k holds
N . x <= N . k
by WAYBEL_0:11;
take
j
;
:: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in V )
let k be
Element of
N;
:: thesis: ( not j <= k or N . k in V )
assume
j <= k
;
:: thesis: N . k in V
then
N . x <= N . k
by A7;
then consider Y being
Subset of
X such that A8:
Y = {(N . k)}
and A9:
N . x in Cl Y
by Def2;
Y meets I
by A2, A4, A6, A9, PRE_TOPC:def 13;
then consider m being
set such that A10:
m in Y /\ I
by XBOOLE_0:4;
A11:
(
m in Y &
m in I )
by A10, XBOOLE_0:def 4;
then A12:
m = N . k
by A8, TARSKI:def 1;
Int V c= V
by TOPS_1:44;
hence
N . k in V
by A11, A12;
:: thesis: verum
end;
hence
sup N in Lim N
by YELLOW_6:def 18; :: thesis: verum