let X be set ; 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; 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; ( 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
; 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 ;
TARSKI:def 3 ( 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
;
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;
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 ;
TARSKI:def 3 ( 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 ) }
;
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;
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; verum