theorem :: UNIFORM2:27

for T being TopSpace holds subbasis_Pervin_quasi_uniformity T c= the entourages of (Pervin_quasi_uniformity T)