for X being set
for SF being Subset-Family of X
for A being Element of SF holds
( id X c= block_Pervin_uniformity A & (block_Pervin_uniformity A) * (block_Pervin_uniformity A) c= block_Pervin_uniformity A )