let T be up-complete Scott TopLattice; :: thesis: 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
let x be Element of T; :: thesis: for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A
let A be upper Subset of T; :: thesis: ( not x in A implies (downarrow x) ` is a_neighborhood of A )
assume A1: not x in A ; :: thesis: (downarrow x) ` is a_neighborhood of A
(downarrow x) ` is open by Th12;
then A2: Int ((downarrow x) `) = (downarrow x) ` by TOPS_1:23;
A misses downarrow x by A1, Th5;
then A c= (downarrow x) ` by SUBSET_1:23;
hence (downarrow x) ` is a_neighborhood of A by A2, CONNSP_2:def 2; :: thesis: verum