let ET be FMT_TopSpace; :: thesis:
let A be non empty Subset of ET; :: thesis:
let V be Subset of ET; :: thesis:
thus ( V is a_neighborhood of A implies ex O being open Subset of ET st
( A c= O & O c= V ) ) :: thesis:

end;

defpred S₁[ object , object ] means ex x being Element of ET ex y being open Subset of ET st
( x = $1 & y = $2 & x in y & y c= V );
A3: for x being object st x in A holds
ex y being object st
( y in bool the carrier of ET & S₁[x,y] )

let x be object ; :: thesis:
assume A4: x in A ; :: thesis:
reconsider x = x as Element of A by A4;
consider O being open Subset of ET such that
A5: x in O and
A6: O c= V by A2;
thus ex y being object st
( y in bool the carrier of ET & S₁[x,y] ) by A5, A6; :: thesis:

end;

ex f being Function of A,(bool the carrier of ET) st
for x being object st x in A holds
S₁[x,f . x] from FUNCT_2:sch 1(A3);
then consider f being Function of A,(bool the carrier of ET) such that
A7: for x being object st x in A holds
S₁[x,f . x] ;
set OO = union (rng f);
( union (rng f) is open Subset of ET & A c= union (rng f) & union (rng f) c= V )

reconsider OO = union (rng f) as Subset of ET ;
A8: ( OO is open Subset of ET & OO c= V )

A9: for a being Element of ET st a in A holds
( f . a is open Subset of ET & f . a c= V )

let a be Element of ET; :: thesis:
assume a in A ; :: thesis:
then S₁[a,f . a] by A7;
then consider x1 being set , y1 being open Subset of ET such that
a = x1 and
A10: f . a = y1 and
x1 in y1 and
A11: y1 c= V ;
thus ( f . a is open Subset of ET & f . a c= V ) by A11, A10; :: thesis:

end;

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in OO ; :: thesis:
then consider T being set such that
A13: t in T and
A14: T in rng f by TARSKI:def 4;
consider x being object such that
A15: x in dom f and
A16: T = f . x by A14, FUNCT_1:def 3;
x in A by A15;
then f . x c= V by A9;
hence t in V by A13, A16; :: thesis:

end;

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in rng f ; :: thesis:
then consider x being object such that
A17: x in dom f and
A18: t = f . x by FUNCT_1:def 3;
A19: x in A by A17;
f . x is open Subset of ET by A19, A9;
hence t in Family_open_set ET by A18; :: thesis:

end;

then union (rng f) in { O where O is open Subset of ET : verum } by Th9;
then consider O1 being open Subset of ET such that
A20: union (rng f) = O1 ;
thus ( OO is open Subset of ET & OO c= V ) by A20, A12; :: thesis:

end;

A c= OO

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A21: t in A ; :: thesis:
then S₁[t,f . t] by A7;
then consider x1, y1 being set such that
A22: t = x1 and
A23: f . t = y1 and
A24: x1 in y1 and
y1 c= V ;
y1 in rng f by A23, A21, FUNCT_2:4;
hence t in OO by A22, A24, TARSKI:def 4; :: thesis:

end;

hence ( union (rng f) is open Subset of ET & A c= union (rng f) & union (rng f) c= V ) by A8; :: thesis:

end;

hence ex O being open Subset of ET st
( A c= O & O c= V ) ; :: thesis:

end;

thus ( ex O being open Subset of ET st
( A c= O & O c= V ) implies V is a_neighborhood of A ) :: thesis:

end;