for X being set
for SF being Subset-Family of X holds basis_Pervin_uniformity SF is axiom_UP1