let X be set ; :: thesis: for SF being Subset-Family of X
for A being Element of SF st not X is empty holds
block_Pervin_uniformity A = { [x,y] where x, y is Element of X : ( x in A iff y in A ) }
let SF be Subset-Family of X; :: thesis: for A being Element of SF st not X is empty holds
block_Pervin_uniformity A = { [x,y] where x, y is Element of X : ( x in A iff y in A ) }
let A be Element of SF; :: thesis: ( not X is empty implies block_Pervin_uniformity A = { [x,y] where x, y is Element of X : ( x in A iff y in A ) } )
assume A1: not X is empty ; :: thesis: block_Pervin_uniformity A = { [x,y] where x, y is Element of X : ( x in A iff y in A ) }
set S = { [x,y] where x, y is Element of X : ( x in A iff y in A ) } ;
A2: block_Pervin_uniformity A c= { [x,y] where x, y is Element of X : ( x in A iff y in A ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in block_Pervin_uniformity A or x in { [x,y] where x, y is Element of X : ( x in A iff y in A ) } )
assume A3: x in block_Pervin_uniformity A ; :: thesis: x in { [x,y] where x, y is Element of X : ( x in A iff y in A ) }
then A4: ( x in [:A,A:] or x in [:(X \ A),(X \ A):] ) by XBOOLE_0:def 3;
consider a, b being object such that
A9: a in X and
A10: b in X and
A11: x = [a,b] by A3, ZFMISC_1:def 2;
( ( a in A & b in A ) or ( a in X \ A & b in X \ A ) ) by A4, A11, ZFMISC_1:87;
then ( ( a in A & b in A ) or ( a in X & not a in A & b in X & not b in A ) ) by XBOOLE_0:def 5;
hence x in { [x,y] where x, y is Element of X : ( x in A iff y in A ) } by A9, A10, A11; :: thesis: verum

end;

{ [x,y] where x, y is Element of X : ( x in A iff y in A ) } c= block_Pervin_uniformity A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [x,y] where x, y is Element of X : ( x in A iff y in A ) } or x in block_Pervin_uniformity A )
assume x in { [x,y] where x, y is Element of X : ( x in A iff y in A ) } ; :: thesis: x in block_Pervin_uniformity A
then consider a, b being Element of X such that
A12: x = [a,b] and
A13: ( a in A iff b in A ) ;
( x in [:A,A:] or ( a in X \ A & b in X \ A ) ) by A1, A13, A12, ZFMISC_1:87, XBOOLE_0:def 5;
then ( x in [:A,A:] or x in [:(X \ A),(X \ A):] ) by A12, ZFMISC_1:87;
hence x in block_Pervin_uniformity A by XBOOLE_0:def 3; :: thesis: verum

end;

hence block_Pervin_uniformity A = { [x,y] where x, y is Element of X : ( x in A iff y in A ) } by A2; :: thesis: verum