:: deftheorem defines block_Pervin_uniformity UNIFORM3:def 28 :
for X being set
for SF being Subset-Family of X
for A being Element of SF holds block_Pervin_uniformity A = [:(X \ A),(X \ A):] \/ [:A,A:];