let ET be FMT_TopSpace; :: thesis: for a being Element of ET

for V being a_neighborhood of a ex O being open Subset of ET st

( a in O & O c= V )

let a be Element of ET; :: thesis: for V being a_neighborhood of a ex O being open Subset of ET st

( a in O & O c= V )

let V be a_neighborhood of a; :: thesis: ex O being open Subset of ET st

( a in O & O c= V )

set O = { x where x is Element of ET : V is a_neighborhood of x } ;

{ x where x is Element of ET : V is a_neighborhood of x } is Subset of ET

A2: O is open Subset of ET

O c= V

( a in O & O c= V ) by A2, A8; :: thesis: verum

for V being a_neighborhood of a ex O being open Subset of ET st

( a in O & O c= V )

let a be Element of ET; :: thesis: for V being a_neighborhood of a ex O being open Subset of ET st

( a in O & O c= V )

let V be a_neighborhood of a; :: thesis: ex O being open Subset of ET st

( a in O & O c= V )

set O = { x where x is Element of ET : V is a_neighborhood of x } ;

{ x where x is Element of ET : V is a_neighborhood of x } is Subset of ET

proof

then reconsider O = { x where x is Element of ET : V is a_neighborhood of x } as Subset of ET ;
{ x where x is Element of ET : V is a_neighborhood of x } c= the carrier of ET

end;proof

hence
{ x where x is Element of ET : V is a_neighborhood of x } is Subset of ET
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of ET : V is a_neighborhood of x } or x in the carrier of ET )

assume x in { x where x is Element of ET : V is a_neighborhood of x } ; :: thesis: x in the carrier of ET

then consider t being Element of ET such that

A1: x = t and

V is a_neighborhood of t ;

thus x in the carrier of ET by A1; :: thesis: verum

end;assume x in { x where x is Element of ET : V is a_neighborhood of x } ; :: thesis: x in the carrier of ET

then consider t being Element of ET such that

A1: x = t and

V is a_neighborhood of t ;

thus x in the carrier of ET by A1; :: thesis: verum

A2: O is open Subset of ET

proof

A8:
a in O
;
for x being Element of ET st x in O holds

O in U_FMT x

end;O in U_FMT x

proof

hence
O is open Subset of ET
by Def1; :: thesis: verum
let x be Element of ET; :: thesis: ( x in O implies O in U_FMT x )

assume x in O ; :: thesis: O in U_FMT x

then consider t being Element of ET such that

A3: x = t and

A4: V is a_neighborhood of t ;

( x is Element of ET & V is Element of U_FMT x ) by A3, A4, Def5;

then consider W being Element of U_FMT x such that

A5: for y being Element of ET st y is Element of W holds

V is Element of U_FMT y by Def4;

A6: W c= O

end;assume x in O ; :: thesis: O in U_FMT x

then consider t being Element of ET such that

A3: x = t and

A4: V is a_neighborhood of t ;

( x is Element of ET & V is Element of U_FMT x ) by A3, A4, Def5;

then consider W being Element of U_FMT x such that

A5: for y being Element of ET st y is Element of W holds

V is Element of U_FMT y by Def4;

A6: W c= O

proof

( W in U_FMT x & U_FMT x is Filter of the carrier of ET )
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in W or v in O )

assume E1: v in W ; :: thesis: v in O

not U_FMT x is empty by Th4;

then W in U_FMT x ;

then reconsider v = v as Element of ET by E1;

A7: ( v is Element of ET & V is Element of U_FMT v ) by E1, A5;

not U_FMT v is empty by Th4;

then V is a_neighborhood of v by A7, Def5;

hence v in O ; :: thesis: verum

end;assume E1: v in W ; :: thesis: v in O

not U_FMT x is empty by Th4;

then W in U_FMT x ;

then reconsider v = v as Element of ET by E1;

A7: ( v is Element of ET & V is Element of U_FMT v ) by E1, A5;

not U_FMT v is empty by Th4;

then V is a_neighborhood of v by A7, Def5;

hence v in O ; :: thesis: verum

proof

hence
O in U_FMT x
by A6, CARD_FIL:def 1; :: thesis: verum
thus
U_FMT x is Filter of the carrier of ET
by Def2; :: thesis: verum

end;O c= V

proof

hence
ex O being open Subset of ET st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in O or x in V )

assume x in O ; :: thesis: x in V

then consider x0 being Element of ET such that

A9: x = x0 and

A10: V is a_neighborhood of x0 ;

V in U_FMT x0 by A10, Def5;

hence x in V by A9, Def3; :: thesis: verum

end;assume x in O ; :: thesis: x in V

then consider x0 being Element of ET such that

A9: x = x0 and

A10: V is a_neighborhood of x0 ;

V in U_FMT x0 by A10, Def5;

hence x in V by A9, Def3; :: thesis: verum

( a in O & O c= V ) by A2, A8; :: thesis: verum