let x, y be set ; :: thesis: ( x in basis_Pervin_quasi_uniformity T & y in basis_Pervin_quasi_uniformity T implies x /\ y in basis_Pervin_quasi_uniformity T )
assume that
A1: x in basis_Pervin_quasi_uniformity T and
A2: y in basis_Pervin_quasi_uniformity T ; :: thesis: x /\ y in basis_Pervin_quasi_uniformity T
consider Y being Subset-Family of [: the carrier of T, the carrier of T:] such that
A3: Y c= subbasis_Pervin_quasi_uniformity T and
A4: Y is finite and
A5: x = Intersect Y by A1, CANTOR_1:def 3;
consider Z being Subset-Family of [: the carrier of T, the carrier of T:] such that
A6: Z c= subbasis_Pervin_quasi_uniformity T and
A7: Z is finite and
A8: y = Intersect Z by A2, CANTOR_1:def 3;
A9: x /\ y = Intersect (Y \/ Z) by A5, A8, MSSUBFAM:8;
Y \/ Z c= subbasis_Pervin_quasi_uniformity T by A3, A6, XBOOLE_1:8;
hence x /\ y in basis_Pervin_quasi_uniformity T by A9, A4, A7, CANTOR_1:def 3; :: thesis: verum