:: deftheorem defines basis_Pervin_quasi_uniformity UNIFORM2:def 23 :
for T being TopSpace holds basis_Pervin_quasi_uniformity T = FinMeetCl (subbasis_Pervin_quasi_uniformity T);