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 )

( A c= O & O c= V ) implies V is a_neighborhood of A ) :: thesis: verum

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

thus
( ex O being open Subset of ET st
assume A1:
V is a_neighborhood of A
; :: thesis: ex O being open Subset of ET st

( A c= O & O c= V )

_{1}[ 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_{1}[x,y] )

for x being object st x in A holds

S_{1}[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_{1}[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 )

( A c= O & O c= V ) ; :: thesis: verum

end;( 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 )

defpred Sex 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 A1, Def6;

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;( 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 A1, Def6;

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

( 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

proof

ex f being Function of A,(bool the carrier of ET) st
let x be object ; :: thesis: ( x in A implies ex y being object st

( y in bool the carrier of ET & S_{1}[x,y] ) )

assume A4: x in A ; :: thesis: ex y being object st

( y in bool the carrier of ET & S_{1}[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 & S_{1}[x,y] )
by A5, A6; :: thesis: verum

end;( y in bool the carrier of ET & S

assume A4: x in A ; :: thesis: ex y being object st

( y in bool the carrier of ET & S

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

for x being object st x in A holds

S

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

set OO = union (rng f);

( union (rng f) is open Subset of ET & A c= union (rng f) & union (rng f) c= V )

proof

hence
ex O being open Subset of ET st
reconsider OO = union (rng f) as Subset of ET ;

A8: ( OO is open Subset of ET & OO c= V )

end;A8: ( OO is open Subset of ET & OO c= V )

proof

A c= OO
A9:
for a being Element of ET st a in A holds

( f . a is open Subset of ET & f . a c= V )

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: verum

end;( f . a is open Subset of ET & f . a c= V )

proof

A12:
OO c= V
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 S_{1}[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: verum

end;assume a in A ; :: thesis: ( f . a is open Subset of ET & f . a c= V )

then S

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: verum

proof

rng f c= Family_open_set ET
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 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: verum

end;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 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: verum

proof

then
union (rng f) in { O where O is open Subset of ET : verum }
by Th9;
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: t in Family_open_set ET

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: verum

end;assume t in rng f ; :: thesis: t in Family_open_set ET

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: verum

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: verum

proof

hence
( union (rng f) is open Subset of ET & A c= union (rng f) & union (rng f) c= V )
by A8; :: thesis: verum
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 S_{1}[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: verum

end;assume A21: t in A ; :: thesis: t in OO

then S

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: verum

( A c= O & O c= V ) ; :: thesis: verum

( 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 A25, Def1;

then O is a_neighborhood of A by Def6;

hence V is a_neighborhood of A by A26, Th7; :: thesis: verum

end;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 A25, Def1;

then O is a_neighborhood of A by Def6;

hence V is a_neighborhood of A by A26, Th7; :: thesis: verum