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