ex US being strict UniformSpace st
( the carrier of US = X & the entourages of US = <.(basis_Pervin_uniformity SF).] ) by Th45;
hence UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #) is strict UniformSpace ; :: thesis: verum