let X be set ; :: thesis: for SF being Subset-Family of X holds basis_Pervin_uniformity SF is axiom_UP1
let SF be Subset-Family of X; :: thesis: basis_Pervin_uniformity SF is axiom_UP1
for B being Element of basis_Pervin_uniformity SF holds id X c= B

proof

let B be Element of basis_Pervin_uniformity SF; :: thesis: id X c= B
B 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: B = Intersect Y by CANTOR_1:def 3;
id X c= B

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in id X or t in B )
assume A3: t in id X ; :: thesis: t in B
then consider a, b being object such that
A4: t = [a,b] by RELAT_1:def 1;
A5: ( a in X & 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 = [:X,X:] 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_uniformity O) where O is Element of SF : verum } by A1;
then consider O being Element of SF such that
A9: y = block_Pervin_uniformity O ;
A10: ( [:(X \ O),(X \ O):] c= y & [:O,O:] c= y ) by A9, XBOOLE_1:10;

per cases ( a in X \ O or a in O ) by A5, XBOOLE_0:def 5;

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

then [a,b] in [:(X \ O),(X \ O):] 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 [:O,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;

end;

hence id X c= B ; :: thesis: verum

end;

hence basis_Pervin_uniformity SF is axiom_UP1 ; :: thesis: verum