let T be non empty up-complete TopPoset; ( T is upper implies T is order_consistent )
assume A1:
T is upper
; T is order_consistent
then reconsider BB = { ((downarrow x) ` ) where x is Element of T : verum } as prebasis of T by Def1;
for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
proof
let x be
Element of
T;
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
A2:
downarrow x c= Cl {x}
Cl {x} c= downarrow x
hence
downarrow x = Cl {x}
by A2, XBOOLE_0:def 10;
for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V
thus
for
N being
eventually-directed net of
T st
x = sup N holds
for
V being
a_neighborhood of
x holds
N is_eventually_in V
verumproof
let N be
eventually-directed net of
T;
( x = sup N implies for V being a_neighborhood of x holds N is_eventually_in V )
assume
x = sup N
;
for V being a_neighborhood of x holds N is_eventually_in V
then A12:
x =
Sup
by WAYBEL_2:def 1
.=
sup (rng (netmap N,T))
by YELLOW_2:def 5
;
let V be
a_neighborhood of
x;
N is_eventually_in V
A13:
x in Int V
by CONNSP_2:def 1;
FinMeetCl BB is
Basis of
T
by YELLOW_9:23;
then A14:
the
topology of
T = UniCl (FinMeetCl BB)
by YELLOW_9:22;
Int V in the
topology of
T
by PRE_TOPC:def 5;
then consider Y being
Subset-Family of
T such that A15:
Y c= FinMeetCl BB
and A16:
Int V = union Y
by A14, CANTOR_1:def 1;
consider Y1 being
set such that A17:
x in Y1
and A18:
Y1 in Y
by A13, A16, TARSKI:def 4;
consider Z being
Subset-Family of
T such that A19:
Z c= BB
and A20:
Z is
finite
and A21:
Y1 = Intersect Z
by A15, A18, CANTOR_1:def 4;
reconsider rngN =
rng (netmap N,T) as
Subset of
T ;
rngN is
directed
by WAYBEL_2:18;
then
ex
a being
Element of
T st
(
a is_>=_than rngN & ( for
b being
Element of
T st
b is_>=_than rngN holds
a <= b ) )
by WAYBEL_0:def 39;
then A22:
ex_sup_of rngN,
T
by YELLOW_0:15;
defpred S1[
set ,
set ]
means for
i,
j being
Element of
N st
i = $2 &
j >= i holds
N . j in $1;
A23:
for
Q being
set st
Q in Z holds
ex
b being
set st
(
b in the
carrier of
N &
S1[
Q,
b] )
proof
let Q be
set ;
( Q in Z implies ex b being set st
( b in the carrier of N & S1[Q,b] ) )
assume A24:
Q in Z
;
ex b being set st
( b in the carrier of N & S1[Q,b] )
then
Q in BB
by A19;
then consider v1 being
Element of
T such that A25:
Q = (downarrow v1) `
;
x in (downarrow v1) `
by A17, A21, A24, A25, SETFAM_1:58;
then
not
x in downarrow v1
by XBOOLE_0:def 5;
then A26:
not
x <= v1
by WAYBEL_0:17;
not
rngN c= downarrow v1
then consider w being
set such that A28:
w in rngN
and A29:
not
w in downarrow v1
by TARSKI:def 3;
reconsider w9 =
w as
Element of
T by A28;
consider i being
set such that A30:
i in dom the
mapping of
N
and A31:
w9 = the
mapping of
N . i
by A28, FUNCT_1:def 5;
reconsider i =
i as
Element of
N by A30;
consider b being
Element of
N such that A32:
for
l being
Element of
N st
b <= l holds
N . i <= N . l
by WAYBEL_0:11;
take
b
;
( b in the carrier of N & S1[Q,b] )
thus
b in the
carrier of
N
;
S1[Q,b]
thus
for
j,
k being
Element of
N st
j = b &
k >= j holds
N . k in Q
verum
end;
consider f being
Function such that A36:
(
dom f = Z &
rng f c= the
carrier of
N )
and A37:
for
Q being
set st
Q in Z holds
S1[
Q,
f . Q]
from WELLORD2:sch 1(A23);
reconsider rngf =
rng f as
finite Subset of
([#] N) by A20, A36, FINSET_1:26;
[#] N is
directed
by WAYBEL_0:def 6;
then consider k being
Element of
N such that
k in [#] N
and A38:
k is_>=_than rngf
by WAYBEL_0:1;
take
k
;
WAYBEL_0:def 11 for b1 being Element of the carrier of N holds
( not k <= b1 or N . b1 in V )
let k1 be
Element of
N;
( not k <= k1 or N . k1 in V )
assume A39:
k <= k1
;
N . k1 in V
then A42:
N . k1 in Y1
by A21, SETFAM_1:58;
Y1 c= union Y
by A18, ZFMISC_1:92;
then A43:
N . k1 in Int V
by A16, A42;
Int V c= V
by TOPS_1:44;
hence
N . k1 in V
by A43;
verum
end;
end;
hence
T is order_consistent
by Def2; verum