let T be non empty TopSpace; for x being Element of subbasis_Pervin_quasi_uniformity T
for y being Element of (Pervin_quasi_uniformity T) holds { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the topology of T
let x be Element of subbasis_Pervin_quasi_uniformity T; for y being Element of (Pervin_quasi_uniformity T) holds { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the topology of T
let y be Element of (Pervin_quasi_uniformity T); { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the topology of T
x in subbasis_Pervin_quasi_uniformity T
;
then consider O being Element of the topology of T such that
A1:
x = block_Pervin_quasi_uniformity O
;
set M = { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } ;
per cases
( y in O or not y in O )
;
suppose A2:
y in O
;
{ z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the topology of T
{ z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } = O
proof
thus
{ z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } c= O
XBOOLE_0:def 10 O c= { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } proof
let a be
object ;
TARSKI:def 3 ( not a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } or a in O )
assume
a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x }
;
a in O
then consider b being
Element of
(Pervin_quasi_uniformity T) such that A4:
b = a
and A5:
[y,b] in x
;
(
[y,b] in [:( the carrier of T \ O), the carrier of T:] or
[y,b] in [: the carrier of T,O:] )
by A1, A5, XBOOLE_0:def 3;
then
( (
y in the
carrier of
T \ O &
b in the
carrier of
T ) or (
y in the
carrier of
T &
b in O ) )
by ZFMISC_1:87;
hence
a in O
by A4, A2, XBOOLE_0:def 5;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in O or a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } )
assume A6:
a in O
;
a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x }
then reconsider b =
a as
Element of
(Pervin_quasi_uniformity T) ;
[y,b] in [: the carrier of T,O:]
by A6, ZFMISC_1:87;
then
[y,b] in [:( the carrier of T \ O), the carrier of T:] \/ [: the carrier of T,O:]
by XBOOLE_0:def 3;
hence
a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x }
by A1;
verum
end; hence
{ z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the
topology of
T
;
verum end; suppose A7:
not
y in O
;
{ z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the topology of T
{ z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } = the
carrier of
(Pervin_quasi_uniformity T)
proof
thus
{ z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } c= the
carrier of
(Pervin_quasi_uniformity T)
XBOOLE_0:def 10 the carrier of (Pervin_quasi_uniformity T) c= { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x }
let a be
object ;
TARSKI:def 3 ( not a in the carrier of (Pervin_quasi_uniformity T) or a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } )
assume
a in the
carrier of
(Pervin_quasi_uniformity T)
;
a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x }
then reconsider b =
a as
Element of the
carrier of
(Pervin_quasi_uniformity T) ;
(
y in the
carrier of
T \ O &
b in the
carrier of
T )
by A7, XBOOLE_0:def 5;
then A10:
[y,b] in [:( the carrier of T \ O), the carrier of T:]
by ZFMISC_1:87;
[:( the carrier of T \ O), the carrier of T:] c= [:( the carrier of T \ O), the carrier of T:] \/ [: the carrier of T,O:]
by XBOOLE_1:7;
hence
a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x }
by A1, A10;
verum
end; hence
{ z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the
topology of
T
by PRE_TOPC:def 1;
verum end; end;