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 ;
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;
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 A11:
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
A12:
x in Int V
by CONNSP_2:def 1;
FinMeetCl BB is
Basis of
T
by YELLOW_9:23;
then A13:
the
topology of
T = UniCl (FinMeetCl BB)
by YELLOW_9:22;
Int V in the
topology of
T
by PRE_TOPC:def 2;
then consider Y being
Subset-Family of
T such that A14:
Y c= FinMeetCl BB
and A15:
Int V = union Y
by A13, CANTOR_1:def 1;
consider Y1 being
set such that A16:
x in Y1
and A17:
Y1 in Y
by A12, A15, TARSKI:def 4;
consider Z being
Subset-Family of
T such that A18:
Z c= BB
and A19:
Z is
finite
and A20:
Y1 = Intersect Z
by A14, A17, CANTOR_1:def 3;
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 A21:
ex_sup_of rngN,
T
by YELLOW_0:15;
defpred S1[
object ,
object ]
means ex
D1 being
set st
(
D1 = $1 & ( for
i,
j being
Element of
N st
i = $2 &
j >= i holds
N . j in D1 ) );
A22:
for
Q being
object st
Q in Z holds
ex
b being
object st
(
b in the
carrier of
N &
S1[
Q,
b] )
proof
let Q be
object ;
( Q in Z implies ex b being object st
( b in the carrier of N & S1[Q,b] ) )
assume A23:
Q in Z
;
ex b being object st
( b in the carrier of N & S1[Q,b] )
then
Q in BB
by A18;
then consider v1 being
Element of
T such that A24:
Q = (downarrow v1) `
;
x in (downarrow v1) `
by A16, A20, A23, A24, SETFAM_1:43;
then
not
x in downarrow v1
by XBOOLE_0:def 5;
then A25:
not
x <= v1
by WAYBEL_0:17;
not
rngN c= downarrow v1
then consider w being
object such that A27:
w in rngN
and A28:
not
w in downarrow v1
;
reconsider w9 =
w as
Element of
T by A27;
consider i being
object such that A29:
i in dom the
mapping of
N
and A30:
w9 = the
mapping of
N . i
by A27, FUNCT_1:def 3;
reconsider i =
i as
Element of
N by A29;
consider b being
Element of
N such that A31:
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]
reconsider QQ =
Q as
set by TARSKI:1;
take
QQ
;
( QQ = Q & ( for i, j being Element of N st i = b & j >= i holds
N . j in QQ ) )
thus
QQ = Q
;
for i, j being Element of N st i = b & j >= i holds
N . j in QQ
thus
for
j,
k being
Element of
N st
j = b &
k >= j holds
N . k in QQ
verum
end;
consider f being
Function such that A35:
(
dom f = Z &
rng f c= the
carrier of
N )
and A36:
for
Q being
object st
Q in Z holds
S1[
Q,
f . Q]
from FUNCT_1:sch 6(A22);
reconsider rngf =
rng f as
finite Subset of
([#] N) by A19, A35, FINSET_1:8;
[#] N is
directed
by WAYBEL_0:def 6;
then consider k being
Element of
N such that
k in [#] N
and A37:
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 A38:
k <= k1
;
N . k1 in V
then A42:
N . k1 in Y1
by A20, SETFAM_1:43;
Y1 c= union Y
by A17, ZFMISC_1:74;
then A43:
N . k1 in Int V
by A15, A42;
Int V c= V
by TOPS_1:16;
hence
N . k1 in V
by A43;
verum
end;
end;
hence
T is order_consistent
; verum