let T be non empty TopSpace; :: thesis: 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; :: thesis: 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); :: thesis: { 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 ; :: thesis: { 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 :: according to XBOOLE_0:def 10 :: thesis: O c= { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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 } ; :: thesis: 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; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

hence { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the topology of T ; :: thesis: verum

end;

suppose A7: not y in O ; :: thesis: { 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) :: according to XBOOLE_0:def 10 :: thesis: the carrier of (Pervin_quasi_uniformity T) c= { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } or a in the carrier of (Pervin_quasi_uniformity T) )
assume a in { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } ; :: thesis: a in the carrier of (Pervin_quasi_uniformity T)
then ex b being Element of (Pervin_quasi_uniformity T) st
( a = b & [y,b] in x ) ;
hence a in the carrier of (Pervin_quasi_uniformity T) ; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

end;