let T be non empty TopSpace; :: thesis: 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)
let V be Subset of [: the carrier of T, the carrier of T:]; :: thesis: ( ex b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) st b c= V implies V is Element of the entourages of (Pervin_quasi_uniformity T) )
given b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) such that A1: b c= V ; :: thesis: V is Element of the entourages of (Pervin_quasi_uniformity T)
A2: <.(basis_Pervin_quasi_uniformity T).] = { x where x is Subset of [: the carrier of T, the carrier of T:] : ex b being Element of basis_Pervin_quasi_uniformity T st b c= x } by CARDFIL2:14;
V in <.(basis_Pervin_quasi_uniformity T).] by A1, A2;
hence V is Element of the entourages of (Pervin_quasi_uniformity T) ; :: thesis: verum