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
proof
{ x where x is Element of ET : V is a_neighborhood of x } c= the carrier of ET
proof
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;
hence { x where x is Element of ET : V is a_neighborhood of x } is Subset of ET ; :: thesis: verum
end;
then reconsider O = { x where x is Element of ET : V is a_neighborhood of x } as Subset of ET ;
A2: O is open Subset of ET
proof
for x being Element of ET st x in O holds
O in U_FMT x
proof
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
proof
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 ;
hence v in O ; :: thesis: verum
end;
( W in U_FMT x & U_FMT x is Filter of the carrier of ET )
proof
hereby :: thesis: U_FMT x is Filter of the carrier of ET
not U_FMT x is empty by Th4;
hence W in U_FMT x ; :: thesis: verum
end;
thus U_FMT x is Filter of the carrier of ET by Def2; :: thesis: verum
end;
hence O in U_FMT x by ; :: thesis: verum
end;
hence O is open Subset of ET by Def1; :: thesis: verum
end;
A8: a in O ;
O c= V
proof
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 ;
hence x in V by ; :: thesis: verum
end;
hence ex O being open Subset of ET st
( a in O & O c= V ) by A2, A8; :: thesis: verum