let X be set ; :: thesis: for SF being Subset-Family of X ex US being strict UniformSpace st
( the carrier of US = X & the entourages of US = <.(basis_Pervin_uniformity SF).] )
let SF be Subset-Family of X; :: thesis: ex US being strict UniformSpace st
( the carrier of US = X & the entourages of US = <.(basis_Pervin_uniformity SF).] )
( basis_Pervin_uniformity SF is quasi_basis & basis_Pervin_uniformity SF is axiom_UP1 & basis_Pervin_uniformity SF is axiom_UP2 & basis_Pervin_uniformity SF is axiom_UP3 ) by Th37, Th38, Th44, Th43;
hence ex US being strict UniformSpace st
( the carrier of US = X & the entourages of US = <.(basis_Pervin_uniformity SF).] ) by Th7; :: thesis: verum