let X be set ; :: thesis: for SF being Subset-Family of X
for R being Relation of X st R is Element of subbasis_Pervin_uniformity SF holds
R ~ is Element of subbasis_Pervin_uniformity SF
let SF be Subset-Family of X; :: thesis: for R being Relation of X st R is Element of subbasis_Pervin_uniformity SF holds
R ~ is Element of subbasis_Pervin_uniformity SF
let R be Relation of X; :: thesis: ( R is Element of subbasis_Pervin_uniformity SF implies R ~ is Element of subbasis_Pervin_uniformity SF )
assume A1: R is Element of subbasis_Pervin_uniformity SF ; :: thesis: R ~ is Element of subbasis_Pervin_uniformity SF
then R in { (block_Pervin_uniformity A) where A is Element of SF : verum } ;
then ex A being Element of SF st R = block_Pervin_uniformity A ;
hence R ~ is Element of subbasis_Pervin_uniformity SF by A1, Th39; :: thesis: verum