:: deftheorem defines Pervin_quasi_uniformity UNIFORM2:def 24 :
for T being TopSpace holds Pervin_quasi_uniformity T = UniformSpaceStr(# the carrier of T,<.(basis_Pervin_quasi_uniformity T).] #);