let X be set ; :: thesis: for SF being Subset-Family of X holds basis_Pervin_uniformity SF is axiom_UP2
let SF be Subset-Family of X; :: thesis: basis_Pervin_uniformity SF is axiom_UP2
let B1 be Element of basis_Pervin_uniformity SF; :: according to UNIFORM3:def 1 :: thesis: ex B2 being Element of basis_Pervin_uniformity SF st B2 c= B1 ~
B1 in FinMeetCl (subbasis_Pervin_uniformity SF) ;
then consider Y being Subset-Family of [:X,X:] such that
A1: Y c= subbasis_Pervin_uniformity SF and
Y is finite and
A2: B1 = Intersect Y by CANTOR_1:def 3;

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

suppose Y is empty ; :: thesis: ex B2 being Element of basis_Pervin_uniformity SF st B2 c= B1 ~

then A3: B1 = [:X,X:] by A2, SETFAM_1:def 9;
B1 c= B1 ~

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B1 or x in B1 ~ )
assume x in B1 ; :: thesis: x in B1 ~
then consider a, b being object such that
A4: a in X and
A5: b in X and
A6: x = [a,b] by A2, ZFMISC_1:def 2;
[b,a] in B1 by A3, A4, A5, ZFMISC_1:def 2;
hence x in B1 ~ by A6, RELAT_1:def 7; :: thesis: verum

end;

hence ex B2 being Element of basis_Pervin_uniformity SF st B2 c= B1 ~ ; :: thesis: verum

end;

suppose A9: not Y is empty ; :: thesis: ex B2 being Element of basis_Pervin_uniformity SF st B2 c= B1 ~

then A10: B1 = meet Y by A2, SETFAM_1:def 9;
set Y2 = Y [~] ;
Y [~] = Y by A1, A9, Th40;
then reconsider B2 = meet (Y [~]) as Element of basis_Pervin_uniformity SF by A9, A2, SETFAM_1:def 9;
B2 c= B1 ~

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B2 or x in B1 ~ )
assume x in B2 ; :: thesis: x in B1 ~
then x in meet Y by A1, A9, Th40;
hence x in B1 ~ by A10, A1, A9, Th42; :: thesis: verum

end;

hence ex B2 being Element of basis_Pervin_uniformity SF st B2 c= B1 ~ ; :: thesis: verum

end;

end;