for US being non empty UniformSpace
for S being Subset of (FMT_induced_by US) holds
( S is open iff for x being Element of US st x in S holds
S in Neighborhood x )