theorem :: UNIFORM3:72

for X being set
for SF being Subset-Family of X
for R being Relation of X st R is Element of subbasis_Pervin_uniformity SF holds
R ~ is Element of subbasis_Pervin_uniformity SF