for US being non empty UniformSpace holds Family_open_set (FMT_induced_by US) = { O where O is open Subset of (FMT_induced_by US) : verum } ;