for US being non empty UniformSpace
for S being Subset of (FMT_induced_by US) holds
( S is open iff S in Family_open_set (FMT_induced_by US) )