let X be set ; :: thesis: 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) ~
let SF be Subset-Family of X; :: thesis: for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds
meet Y = (meet Y) ~
let Y be non empty Subset-Family of [:X,X:]; :: thesis: ( Y c= subbasis_Pervin_uniformity SF implies meet Y = (meet Y) ~ )
assume A1: Y c= subbasis_Pervin_uniformity SF ; :: thesis: meet Y = (meet Y) ~
then meet (Y [~]) = meet Y by Th40;
hence meet Y = (meet Y) ~ by A1, Th41; :: thesis: verum