now for x, y being set st x in basis_Pervin_quasi_uniformity T & y in basis_Pervin_quasi_uniformity T holds
x /\ y in basis_Pervin_quasi_uniformity Tlet x,
y be
set ;
( 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
;
x /\ y in basis_Pervin_quasi_uniformity Tconsider 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;
verum end;
hence
basis_Pervin_quasi_uniformity T is cap-closed
by FINSUB_1:def 2; verum