theorem :: UNIFORM3:66

for X being set
for SF being Subset-Family of X
for A being Element of SF st not X is empty holds
block_Pervin_uniformity A = { [x,y] where x, y is Element of X : ( x in A iff y in A ) }