for US being non empty UniformSpace holds
( the carrier of (TopSpace_induced_by US) = the carrier of US & the topology of (TopSpace_induced_by US) = Family_open_set (FMT_induced_by US) ) by FINTOPO7:def 16;