let X be set ; :: thesis: for SF being Subset-Family of X
for A being Element of SF
for R being Relation of X st R = block_Pervin_uniformity A holds
R ~ = block_Pervin_uniformity A
let SF be Subset-Family of X; :: thesis: for A being Element of SF
for R being Relation of X st R = block_Pervin_uniformity A holds
R ~ = block_Pervin_uniformity A
let A be Element of SF; :: thesis: for R being Relation of X st R = block_Pervin_uniformity A holds
R ~ = block_Pervin_uniformity A
let R be Relation of X; :: thesis: ( R = block_Pervin_uniformity A implies R ~ = block_Pervin_uniformity A )
assume A1: R = block_Pervin_uniformity A ; :: thesis: R ~ = block_Pervin_uniformity A
per cases ( SF is empty or not SF is empty ) ;
suppose SF is empty ; :: thesis: R ~ = block_Pervin_uniformity A
then F1: A = {} by SUBSET_1:def 1;
then R = [:X,X:] by A1, Th34;
then R ~ = [:X,X:] by SYSREL:5;
hence R ~ = block_Pervin_uniformity A by F1, Th34; :: thesis: verum
end;
suppose not SF is empty ; :: thesis: R ~ = block_Pervin_uniformity A
then A in SF ;
then reconsider A = A as Subset of X ;
R ~ = [:A,A:] \/ [:(X \ A),(X \ A):] by A1, Th33;
hence R ~ = block_Pervin_uniformity A ; :: thesis: verum
end;
end;