let T be non empty TopSpace; :: thesis: for V being Element of the entourages of (Pervin_quasi_uniformity T) ex b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) st b c= V
let V be Element of the entourages of (Pervin_quasi_uniformity T); :: thesis: ex b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) st b c= V
A1: <.(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).] ;
then ex S being Subset of [: the carrier of T, the carrier of T:] st
( V = S & ex b being Element of basis_Pervin_quasi_uniformity T st b c= S ) by A1;
hence ex b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) st b c= V ; :: thesis: verum