theorem Th42: :: UNIFORM3:75

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
meet Y = (meet Y) ~