theorem Th40: :: UNIFORM3:73

for X being set
for SF being Subset-Family of X
for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds
Y [~] = Y