theorem :: UNIFORM3:21

for US being non empty UniformSpace
for S being Subset of (FMT_induced_by US) holds
( S in Family_open_set (FMT_induced_by US) iff for x being Element of US st x in S holds
S in Neighborhood x ) by Th8, Th9;