let T be non empty strict TopSpace; :: thesis: TopSpace_induced_by (Pervin_quasi_uniformity T) = T
the topology of (TopSpace_induced_by (Pervin_quasi_uniformity T)) = Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T)) by FINTOPO7:def 16;
hence TopSpace_induced_by (Pervin_quasi_uniformity T) = T by FINTOPO7:def 16, Th32; :: thesis: verum