let B be Element of basis_Pervin_quasi_uniformity T; :: according to UNIFORM2:def 16 :: thesis: id the carrier of T c= B
B in FinMeetCl (subbasis_Pervin_quasi_uniformity T) ;
then consider Y being Subset-Family of [: the carrier of T, the carrier of T:] such that
A1: Y c= subbasis_Pervin_quasi_uniformity T and
Y is finite and
A2: B = Intersect Y by CANTOR_1:def 3;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in id the carrier of T or t in B )
assume A3: t in id the carrier of T ; :: thesis: t in B
then consider a, b being object such that
A4: t = [a,b] by RELAT_1:def 1;
A5: ( a in the carrier of T & a = b ) by A3, A4, RELAT_1:def 10;

per cases ( Y is empty or not Y is empty ) ;

suppose Y is empty ; :: thesis: t in B

then B = [: the carrier of T, the carrier of T:] by A2, SETFAM_1:def 9;
hence t in B by A3; :: thesis: verum

end;

suppose A7: not Y is empty ; :: thesis: t in B

then A8: Intersect Y = meet Y by SETFAM_1:def 9;

now :: thesis: for y being set st y in Y holds
t in y

let y be set ; :: thesis: ( y in Y implies t in b₁ )
assume y in Y ; :: thesis: t in b₁
then y in { (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum } by A1;
then consider O being Element of the topology of T such that
A9: y = block_Pervin_quasi_uniformity O ;
A10: ( [:( the carrier of T \ O), the carrier of T:] c= y & [: the carrier of T,O:] c= y ) by A9, XBOOLE_1:10;

per cases ( a in the carrier of T \ O or a in O ) by A5, XBOOLE_0:def 5;

suppose a in the carrier of T \ O ; :: thesis: t in b₁

then [a,b] in [:( the carrier of T \ O), the carrier of T:] by A5, ZFMISC_1:def 2;
hence t in y by A4, A10; :: thesis: verum

end;

suppose a in O ; :: thesis: t in b₁

then [a,b] in [: the carrier of T,O:] by A5, ZFMISC_1:def 2;
hence t in y by A4, A10; :: thesis: verum

end;

end;

end;

hence t in B by A2, A8, A7, SETFAM_1:def 1; :: thesis: verum

end;

end;