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

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

let V be Subset of ET; :: thesis: ( V is a_neighborhood of A iff ex O being open Subset of ET st
( A c= O & O c= V ) )

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

A2: now :: thesis: for a being Element of ET st a in A holds
ex O being open Subset of ET st
( a in O & O c= V )
let a be Element of ET; :: thesis: ( a in A implies ex O being open Subset of ET st
( a in O & O c= V ) )

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

then V in U_FMT a by ;
then V is a_neighborhood of a by Def5;
hence ex O being open Subset of ET st
( a in O & O c= V ) by Th10; :: thesis: verum
end;
defpred S1[ 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 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in A implies ex y being object st
( y in bool the carrier of ET & S1[x,y] ) )

assume A4: x in A ; :: thesis: ex y being object st
( y in bool the carrier of ET & S1[x,y] )

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 & S1[x,y] ) by A5, A6; :: thesis: verum
end;
ex f being Function of A,(bool the carrier of ET) st
for x being object st x in A holds
S1[x,f . x] from then consider f being Function of A,(bool the carrier of ET) such that
A7: for x being object st x in A holds
S1[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 )
proof
reconsider OO = union (rng f) as Subset of ET ;
A8: ( OO is open Subset of ET & OO c= V )
proof
A9: for a being Element of ET st a in A holds
( f . a is open Subset of ET & f . a c= V )
proof
let a be Element of ET; :: thesis: ( a in A implies ( f . a is open Subset of ET & f . a c= V ) )
assume a in A ; :: thesis: ( f . a is open Subset of ET & f . a c= V )
then S1[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 ; :: thesis: verum
end;
A12: OO c= V
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in OO or t in V )
assume t in OO ; :: thesis: t in V
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 ;
x in A by A15;
then f . x c= V by A9;
hence t in V by ; :: thesis: verum
end;
rng f c= Family_open_set ET
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng f or t in Family_open_set ET )
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 ;
hence t in Family_open_set ET by A18; :: thesis: verum
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 ; :: thesis: verum
end;
A c= OO
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in A or t in OO )
assume A21: t in A ; :: thesis: t in OO
then S1[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 ;
hence t in OO by ; :: thesis: verum
end;
hence ( union (rng f) is open Subset of ET & A c= union (rng f) & union (rng f) c= V ) by A8; :: thesis: verum
end;
hence ex O being open Subset of ET st
( A c= O & O c= V ) ; :: thesis: verum
end;
thus ( ex O being open Subset of ET st
( A c= O & O c= V ) implies V is a_neighborhood of A ) :: thesis: verum
proof
given O being open Subset of ET such that A25: A c= O and
A26: O c= V ; :: thesis: V is a_neighborhood of A
for x being Element of ET st x in A holds
O in U_FMT x by ;
then O is a_neighborhood of A by Def6;
hence V is a_neighborhood of A by ; :: thesis: verum
end;