let T be non empty TopSpace; :: thesis: for ET being FMT_TopSpace st the carrier of T = the carrier of ET & Family_open_set ET = the topology of T holds
for x being Element of ET holds U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) }
let ET be FMT_TopSpace; :: thesis: ( the carrier of T = the carrier of ET & Family_open_set ET = the topology of T implies for x being Element of ET holds U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } )
assume that
the carrier of T = the carrier of ET and
A1: Family_open_set ET = the topology of T ; :: thesis: for x being Element of ET holds U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) }
A2: for o being set st o in Family_open_set ET holds
for x being Element of ET st x in o holds
o in U_FMT x

proof

let o be set ; :: thesis: ( o in Family_open_set ET implies for x being Element of ET st x in o holds
o in U_FMT x )
assume o in Family_open_set ET ; :: thesis: for x being Element of ET st x in o holds
o in U_FMT x
then consider O being open Subset of ET such that
A3: o = O ;
thus for x being Element of ET st x in o holds
o in U_FMT x by A3, Def1; :: thesis: verum

end;

for x being Element of ET holds U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) }

proof

let x be Element of ET; :: thesis: U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) }
A4: U_FMT x c= { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) }

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in U_FMT x or t in { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } )
assume A5: t in U_FMT x ; :: thesis: t in { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) }
then A6: t is a_neighborhood of x by Def5;
reconsider t = t as Subset of ET by A5;
consider OO being open Subset of ET such that
A7: x in OO and
A8: OO c= t by A6, Th10;
A9: OO in Family_open_set ET ;
then reconsider OO = OO as Subset of T by A1;
thus t in { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } by A7, A8, A9, A1; :: thesis: verum

end;

{ V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } c= U_FMT x

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } or t in U_FMT x )
assume t in { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } ; :: thesis: t in U_FMT x
then consider V being Subset of ET such that
A10: t = V and
A11: ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) ;
consider O2 being Subset of T such that
A12: O2 in the topology of T and
A13: x in O2 and
A14: O2 c= V by A11;
A15: O2 in U_FMT x by A12, A1, A2, A13;
U_FMT x is Filter of the carrier of ET by Def2;
hence t in U_FMT x by A14, CARD_FIL:def 1, A15, A10; :: thesis: verum

end;

hence U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } by A4; :: thesis: verum

end;

hence for x being Element of ET holds U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
( O in the topology of T & x in O & O c= V ) } ; :: thesis: verum