let X be set ; :: thesis: for SF being Subset-Family of X holds basis_Pervin_uniformity SF is V288()
let SF be Subset-Family of X; :: thesis: basis_Pervin_uniformity SF is V288()

now :: thesis: for x, y being set st x in basis_Pervin_uniformity SF & y in basis_Pervin_uniformity SF holds
x /\ y in basis_Pervin_uniformity SF

let x, y be set ; :: thesis: ( x in basis_Pervin_uniformity SF & y in basis_Pervin_uniformity SF implies x /\ y in basis_Pervin_uniformity SF )
assume that
A1: x in basis_Pervin_uniformity SF and
A2: y in basis_Pervin_uniformity SF ; :: thesis: x /\ y in basis_Pervin_uniformity SF
consider Y being Subset-Family of [:X,X:] such that
A3: Y c= subbasis_Pervin_uniformity SF and
A4: Y is finite and
A5: x = Intersect Y by A1, CANTOR_1:def 3;
consider Z being Subset-Family of [:X,X:] such that
A6: Z c= subbasis_Pervin_uniformity SF 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_uniformity SF by A3, A6, XBOOLE_1:8;
hence x /\ y in basis_Pervin_uniformity SF by A9, A4, A7, CANTOR_1:def 3; :: thesis: verum

end;

hence basis_Pervin_uniformity SF is V288() ; :: thesis: verum