theorem Th13: :: WAYBEL11:13

for T being up-complete Scott TopLattice
for x being Element of T
for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A