let X be set ; :: thesis: for SF being Subset-Family of X holds basis_Pervin_uniformity SF is axiom_UP3
let SF be Subset-Family of X; :: thesis: basis_Pervin_uniformity SF is axiom_UP3
for B1 being Element of basis_Pervin_uniformity SF ex B2 being Element of basis_Pervin_uniformity SF st B2 [*] B2 c= B1

proof

let B1 be Element of basis_Pervin_uniformity SF; :: thesis: ex B2 being Element of basis_Pervin_uniformity SF st B2 [*] 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 [*] B2 c= B1

then A3: B1 = [:X,X:] by A2, SETFAM_1:def 9;
take B1 ; :: thesis: B1 [*] B1 c= B1
thus B1 [*] B1 c= B1 by A3; :: thesis: verum

end;

suppose A4: not Y is empty ; :: thesis: ex B2 being Element of basis_Pervin_uniformity SF st B2 [*] B2 c= B1

then A5: B1 = meet Y by A2, SETFAM_1:def 9;
reconsider B2 = B1 as Element of basis_Pervin_uniformity SF ;
take B2 ; :: thesis: B2 [*] B2 c= B1
B2 * B2 c= B1

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B2 * B2 or t in B1 )
assume A6: t in B2 * B2 ; :: thesis: t in B1
then consider a, b being object such that
A10: t = [a,b] by RELAT_1:def 1;
consider c being object such that
A11: [a,c] in B1 and
A12: [c,b] in B1 by A6, A10, RELAT_1:def 8;
t in B1

proof

for Z being set st Z in Y holds
t in Z

proof

let Z be set ; :: thesis: ( Z in Y implies t in Z )
assume A13: Z in Y ; :: thesis: t in Z
then Z in { (block_Pervin_uniformity O) where O is Element of SF : verum } by A1;
then consider O being Element of SF such that
A14: Z = block_Pervin_uniformity O ;
[a,c] in meet Y by A4, A2, SETFAM_1:def 9, A11;
then A15: [a,c] in block_Pervin_uniformity O by A14, A13, SETFAM_1:def 1;
[c,b] in block_Pervin_uniformity O by A12, A5, A14, A13, SETFAM_1:def 1;
then A16: [a,b] in (block_Pervin_uniformity O) * (block_Pervin_uniformity O) by A15, RELAT_1:def 8;
(block_Pervin_uniformity O) * (block_Pervin_uniformity O) c= block_Pervin_uniformity O by Th35;
hence t in Z by A14, A10, A16; :: thesis: verum

end;

hence t in B1 by A5, A4, SETFAM_1:def 1; :: thesis: verum

end;

hence t in B1 ; :: thesis: verum

end;

hence B2 [*] B2 c= B1 ; :: thesis: verum

end;

end;

end;

hence basis_Pervin_uniformity SF is axiom_UP3 ; :: thesis: verum