let R be non empty reflexive transitive antisymmetric up-complete RelStr ; :: thesis: for T being Scott TopAugmentation of R
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 T be Scott TopAugmentation of R; :: 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 closed by WAYBEL11:11;
then (downarrow x) ` is open ;
then A2: Int ((downarrow x) `) = (downarrow x) ` by TOPS_1:23;
A misses downarrow x by A1, WAYBEL11:5;
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