let B1 be Element of basis_Pervin_quasi_uniformity T; UNIFORM2:def 17 ex B2 being Element of basis_Pervin_quasi_uniformity T st B2 [*] B2 c= B1
B1 in FinMeetCl (subbasis_Pervin_quasi_uniformity T)
;
then consider Y being Subset-Family of [: the carrier of T, the carrier of T:] such that
A1:
Y c= subbasis_Pervin_quasi_uniformity T
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 A4:
not
Y is
empty
;
ex B2 being Element of basis_Pervin_quasi_uniformity T st B2 [*] B2 c= B1then A5:
B1 = meet Y
by A2, SETFAM_1:def 9;
reconsider B2 =
B1 as
Element of
basis_Pervin_quasi_uniformity T ;
take
B2
;
B2 [*] B2 c= B1let t be
object ;
TARSKI:def 3 ( not t in B2 [*] B2 or t in B1 )assume A6:
t in B2 * B2
;
t in B1consider a,
b being
object such that A10:
t = [a,b]
by A6, RELAT_1:def 1;
consider c being
object such that A11:
[a,c] in B2
and A12:
[c,b] in B2
by A6, A10, RELAT_1:def 8;
thus
t in B1
verumproof
for
Z being
set st
Z in Y holds
t in Z
proof
let Z be
set ;
( Z in Y implies t in Z )
assume A13:
Z in Y
;
t in Z
then
Z in { (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum }
by A1;
then consider O being
Element of the
topology of
T such that A14:
Z = block_Pervin_quasi_uniformity O
;
[a,c] in meet Y
by A4, A2, SETFAM_1:def 9, A11;
then A15:
[a,c] in block_Pervin_quasi_uniformity O
by A14, A13, SETFAM_1:def 1;
[c,b] in block_Pervin_quasi_uniformity O
by A12, A5, A14, A13, SETFAM_1:def 1;
then A16:
[a,b] in (block_Pervin_quasi_uniformity O) * (block_Pervin_quasi_uniformity O)
by A15, RELAT_1:def 8;
(block_Pervin_quasi_uniformity O) * (block_Pervin_quasi_uniformity O) c= block_Pervin_quasi_uniformity O
by Th20;
hence
t in Z
by A14, A10, A16;
verum
end;
hence
t in B1
by A5, A4, SETFAM_1:def 1;
verum
end; end;