let R be non empty reflexive transitive antisymmetric up-complete TopRelStr ; :: thesis:
let T be Scott TopAugmentation of R; :: thesis:
let S be upper Subset of T; :: thesis:
defpred S₁[ set ] means $1 is a_neighborhood of S;
set F = { X where X is Subset of T : S₁[X] } ;
{ X where X is Subset of T : S₁[X] } is Subset-Family of T from DOMAIN_1:sch 7();
then reconsider F = { X where X is Subset of T : S₁[X] } as Subset-Family of T ;
take F ; :: thesis:
thus S = meet F :: thesis:

[#] T is a_neighborhood of S by CONNSP_2:28;
then A1: [#] T in F ;

let Z1 be set ; :: thesis:
assume Z1 in F ; :: thesis:
then ex X being Subset of T st
( Z1 = X & X is a_neighborhood of S ) ;
hence S c= Z1 by CONNSP_2:29; :: thesis:

end;

hence S c= meet F by A1, SETFAM_1:5; :: according to XBOOLE_0:def 10 :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume that
A2: x in meet F and
A3: not x in S ; :: thesis:
reconsider p = x as Element of T by A2;
(downarrow p) ` is a_neighborhood of S by A3, Th14;
then (downarrow p) ` in F ;
then A4: meet F c= (downarrow p) ` by SETFAM_1:3;
p <= p ;
then p in downarrow p by WAYBEL_0:17;
hence contradiction by A2, A4, XBOOLE_0:def 5; :: thesis:

end;

let X be Subset of T; :: thesis:
assume X in F ; :: thesis:
then ex Y being Subset of T st
( X = Y & Y is a_neighborhood of S ) ;
hence X is a_neighborhood of S ; :: thesis: