let T be TopSpace; :: thesis: subbasis_Pervin_quasi_uniformity T c= the entourages of (Pervin_quasi_uniformity T)
now :: thesis: for x being object st x in subbasis_Pervin_quasi_uniformity T holds
x in the entourages of (Pervin_quasi_uniformity T)
let x be object ; :: thesis: ( x in subbasis_Pervin_quasi_uniformity T implies x in the entourages of (Pervin_quasi_uniformity T) )
assume A1: x in subbasis_Pervin_quasi_uniformity T ; :: thesis: x in the entourages of (Pervin_quasi_uniformity T)
A2: subbasis_Pervin_quasi_uniformity T c= basis_Pervin_quasi_uniformity T by CANTOR_1:4;
basis_Pervin_quasi_uniformity T c= <.(basis_Pervin_quasi_uniformity T).] by CARDFIL2:18;
hence x in the entourages of (Pervin_quasi_uniformity T) by A1, A2; :: thesis: verum
end;
hence subbasis_Pervin_quasi_uniformity T c= the entourages of (Pervin_quasi_uniformity T) ; :: thesis: verum