theorem Th29: :: UNIFORM2:30

for T being non empty TopSpace
for x being Element of subbasis_Pervin_quasi_uniformity T
for y being Element of (Pervin_quasi_uniformity T) holds { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the topology of T