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 x = sup N ; :: thesis: for V being a_neighborhood of x holds N is_eventually_in V
then x = Sup by WAYBEL_2:def 1;
then A1: 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
A2: x in Int V by CONNSP_2:def 1;
reconsider rngN = rng (netmap (N,T)) as Subset of T ;
rngN is directed by WAYBEL_2:18;
then Int V meets rngN by A1, A2, WAYBEL11:def 1;
then consider z being object such that
A3: z in Int V and
A4: z in rngN by XBOOLE_0:3;
reconsider z9 = z as Element of T by A3;
consider i being object such that
A5: i in dom the mapping of N and
A6: z9 = the mapping of N . i by A4, FUNCT_1:def 3;
reconsider i = i 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 . i <= N . k by WAYBEL_0:11;
take j ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not j <= b₁ or N . b₁ in V )
let l be Element of N; :: thesis: ( not j <= l or N . l in V )
assume j <= l ; :: thesis: N . l in V
then N . i <= N . l by A7;
then A8: N . l in Int V by A3, A6, WAYBEL_0:def 20;
Int V c= V by TOPS_1:16;
hence N . l in V by A8; :: 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 Th5; :: thesis: verum

end;

hence T is order_consistent ; :: thesis: verum