:: deftheorem Def2 defines order_consistent WAYBEL32:def 2 :
for T being non empty TopSpace-like reflexive TopRelStr holds
( T is order_consistent iff 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 ) ) );