let T be non empty up-complete Scott TopPoset; :: thesis: T is order_consistent
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;
:: thesis: ( 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 ) )
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 N be
eventually-directed net of
T;
:: thesis: ( x = sup N implies for V being a_neighborhood of x holds N is_eventually_in V )
assume A1:
x = sup N
;
:: thesis: for V being a_neighborhood of x holds N is_eventually_in V
x = Sup
by A1, WAYBEL_2:def 1;
then A2:
x = sup (rng the mapping of N)
by YELLOW_2:def 5;
let V be
a_neighborhood of
x;
:: thesis: N is_eventually_in V
A3:
x in Int V
by CONNSP_2:def 1;
A4:
Int V is
open
by TOPS_1:51;
then A5:
Int V is
inaccessible_by_directed_joins
;
A6:
Int V is
upper Subset of
T
by A4;
reconsider rngN =
rng (netmap N,T) as
Subset of
T ;
rngN is
directed
by WAYBEL_2:18;
then
Int V meets rngN
by A2, A3, A5, WAYBEL11:def 1;
then consider z being
set such that A7:
(
z in Int V &
z in rngN )
by XBOOLE_0:3;
reconsider z' =
z as
Element of
T by A7;
consider i being
set such that A8:
i in dom the
mapping of
N
and A9:
z' = the
mapping of
N . i
by A7, FUNCT_1:def 5;
reconsider i =
i as
Element of
N by A8;
consider j being
Element of
N such that A10:
for
k being
Element of
N st
j <= k holds
N . i <= 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 l be
Element of
N;
:: thesis: ( not j <= l or N . l in V )
assume A11:
j <= l
;
:: thesis: N . l in V
N . i <= N . l
by A10, A11;
then A12:
N . l in Int V
by A6, A7, A9, WAYBEL_0:def 20;
Int V c= V
by TOPS_1:44;
hence
N . l in V
by A12;
:: thesis: verum
end;
hence
(
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 ) )
by Th9;
:: thesis: verum
end;
hence
T is order_consistent
by Def2; :: thesis: verum