let X be set ; :: thesis:
let A be Subset of X; :: thesis:
thus id X c= block_Pervin_quasi_uniformity A :: thesis:

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: t in id X ; :: thesis:
then consider a, b being object such that
A2: t = [a,b] by RELAT_1:def 1;
A3: ( a in X & a = b ) by A1, A2, RELAT_1:def 10;

per cases ;

suppose a in A ; :: thesis:

then ( a in A & b in A ) by A1, A2, RELAT_1:def 10;
then A4: [a,b] in [:A,A:] by ZFMISC_1:def 2;
A5: [:A,A:] c= [:X,A:] by ZFMISC_1:96;
[:X,A:] c= block_Pervin_quasi_uniformity A by XBOOLE_1:7;
hence t in block_Pervin_quasi_uniformity A by A4, A2, A5; :: thesis:

end;

suppose not a in A ; :: thesis:

then a in X \ A by A3, XBOOLE_0:def 5;
then A6: t in [:(X \ A),X:] by A2, A3, ZFMISC_1:def 2;
[:(X \ A),X:] c= block_Pervin_quasi_uniformity A by XBOOLE_1:7;
hence t in block_Pervin_quasi_uniformity A by A6; :: thesis:

end;

end;

end;

now :: thesis:

let t be object ; :: thesis:
assume A7: t in (block_Pervin_quasi_uniformity A) * (block_Pervin_quasi_uniformity A) ; :: thesis:
then consider a, b being object such that
A8: t = [a,b] by RELAT_1:def 1;
[a,b] in { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in block_Pervin_quasi_uniformity A & [z,y] in block_Pervin_quasi_uniformity A ) } by A8, A7, Th3;
then consider x, y being Element of X such that
A9: [a,b] = [x,y] and
A10: ex z being Element of X st
( [x,z] in block_Pervin_quasi_uniformity A & [z,y] in block_Pervin_quasi_uniformity A ) ;
consider z being Element of X such that
A11: [x,z] in block_Pervin_quasi_uniformity A and
A12: [z,y] in block_Pervin_quasi_uniformity A by A10;

per cases ;

suppose A13: x in A ; :: thesis:

[x,z] in [:A,A:]

proof

per cases in [:(X \ A),X:] or [x,z] in [:X,A:] ) by A11, XBOOLE_0:def 3;

suppose [x,z] in [:(X \ A),X:] ; :: thesis:

then x in X \ A by ZFMISC_1:87;
hence [x,z] in [:A,A:] by A13, XBOOLE_0:def 5; :: thesis:

end;

suppose [x,z] in [:X,A:] ; :: thesis:

then ( x in X & z in A ) by ZFMISC_1:87;
hence [x,z] in [:A,A:] by A13, ZFMISC_1:87; :: thesis:

end;

end;

end;

then A14: z in A by ZFMISC_1:87;
[z,y] in [:A,A:]

proof

per cases in [:(X \ A),X:] or [z,y] in [:X,A:] ) by A12, XBOOLE_0:def 3;

suppose [z,y] in [:(X \ A),X:] ; :: thesis:

then ( z in X \ A & y in X ) by ZFMISC_1:87;
hence [z,y] in [:A,A:] by A14, XBOOLE_0:def 5; :: thesis:

end;

suppose [z,y] in [:X,A:] ; :: thesis:

then y in A by ZFMISC_1:87;
hence [z,y] in [:A,A:] by A14, ZFMISC_1:87; :: thesis:

end;

end;

end;

then y in A by ZFMISC_1:87;
then A15: [x,y] in [:X,A:] by ZFMISC_1:def 2;
[:X,A:] c= block_Pervin_quasi_uniformity A by XBOOLE_1:7;
hence t in block_Pervin_quasi_uniformity A by A8, A9, A15; :: thesis:

end;

suppose A16: not x in A ; :: thesis:

per cases ;

suppose X is empty ; :: thesis:

hence t in block_Pervin_quasi_uniformity A by A12; :: thesis:

end;

suppose not X is empty ; :: thesis:

then x in X \ A by A16, XBOOLE_0:def 5;
then A17: t in [:(X \ A),X:] by A8, A9, ZFMISC_1:87;
[:(X \ A),X:] c= block_Pervin_quasi_uniformity A by XBOOLE_1:7;
hence t in block_Pervin_quasi_uniformity A by A17; :: thesis:

end;

end;

end;

end;

end;

hence (block_Pervin_quasi_uniformity A) * (block_Pervin_quasi_uniformity A) c= block_Pervin_quasi_uniformity A ; :: thesis: