theorem :: UNIFORM2:26

for T being non empty TopSpace
for V being Subset of [: the carrier of T, the carrier of T:] st ex b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) st b c= V holds
V is Element of the entourages of (Pervin_quasi_uniformity T)