:: deftheorem defines subbasis_Pervin_quasi_uniformity UNIFORM2:def 22 :
for T being TopSpace holds subbasis_Pervin_quasi_uniformity T = { (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum } ;