let X be set ; :: thesis: for SF being Subset-Family of X holds basis_Pervin_uniformity SF is quasi_basis
let SF be Subset-Family of X; :: thesis: basis_Pervin_uniformity SF is quasi_basis
basis_Pervin_uniformity SF is V288() by Th36;
hence basis_Pervin_uniformity SF is quasi_basis ; :: thesis: verum