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 A7, Def5;
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 A6, CARD_FIL:def 1; :: 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 A10, Def5;
hence x in V by A9, Def3; :: thesis: verum

end;

hence ex O being open Subset of ET st
( a in O & O c= V ) by A2, A8; :: thesis: verum