theorem Th13: :: FINTOPO7:20

for T being non empty TopSpace
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 ) }