theorem Th43: :: UNIFORM3:76

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