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 ; :: 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 ;
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 ; :: 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