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

( O in the topology of T & x in O & O c= V ) }

( O in the topology of T & x in O & O c= V ) } ; :: thesis: verum

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

for x being Element of ET holds U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
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;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

( O in the topology of T & x in O & O c= V ) }

proof

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
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 ) }

( O in the topology of T & x in O & O c= V ) } c= U_FMT x

( O in the topology of T & x in O & O c= V ) } by A4; :: thesis: verum

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

{ V where V is Subset of ET : ex O being Subset of T st
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;( 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

( O in the topology of T & x in O & O c= V ) } c= U_FMT x

proof

hence
U_FMT x = { V where V is Subset of ET : ex O being Subset of T st
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;( 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

( O in the topology of T & x in O & O c= V ) } by A4; :: thesis: verum

( O in the topology of T & x in O & O c= V ) } ; :: thesis: verum