let X be set ; :: thesis: for SF being Subset-Family of X
for A being Element of SF st A = {} holds
block_Pervin_uniformity A = [:X,X:]
let SF be Subset-Family of X; :: thesis: for A being Element of SF st A = {} holds
block_Pervin_uniformity A = [:X,X:]
let A be Element of SF; :: thesis: ( A = {} implies block_Pervin_uniformity A = [:X,X:] )
assume A = {} ; :: thesis: block_Pervin_uniformity A = [:X,X:]
then block_Pervin_uniformity A = [:(X \ {}),(X \ {}):] \/ [:{},{}:] ;
hence block_Pervin_uniformity A = [:X,X:] ; :: thesis: verum