:: deftheorem defines subbasis_Pervin_uniformity UNIFORM3:def 29 :
for X being set
for SF being Subset-Family of X holds subbasis_Pervin_uniformity SF = { (block_Pervin_uniformity A) where A is Element of SF : verum } ;