:: deftheorem defines Pervin_uniform_space UNIFORM3:def 31 :
for X being set
for SF being Subset-Family of X holds Pervin_uniform_space SF = UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #);