:: deftheorem defines basis_Pervin_uniformity UNIFORM3:def 30 :
for X being set
for SF being Subset-Family of X holds basis_Pervin_uniformity SF = FinMeetCl (subbasis_Pervin_uniformity SF);