let T be non empty TopSpace; :: thesis: Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T)) = the topology of T
A1: Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T)) c= the topology of T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T)) or x in the topology of T )
assume x in Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T)) ; :: thesis: x in the topology of T
then consider O being open Subset of (FMT_induced_by (Pervin_quasi_uniformity T)) such that
A2: x = O ;
reconsider O1 = O as Subset of T ;
for x being set holds
( x in O1 iff ex B being Subset of T st
( B is open & B c= O1 & x in B ) )

proof

let x be set ; :: thesis: ( x in O1 iff ex B being Subset of T st
( B is open & B c= O1 & x in B ) )

hereby :: thesis: ( ex B being Subset of T st
( B is open & B c= O1 & x in B ) implies x in O1 )

assume A3: x in O1 ; :: thesis: ex B being Subset of T st
( B is open & B c= O1 & x in B )
then reconsider t = x as Element of (FMT_induced_by (Pervin_quasi_uniformity T)) ;
consider y being Element of the carrier of (Pervin_quasi_uniformity T) such that
A4: t = y and
A5: U_FMT t = Neighborhood y by Th31;
O in Neighborhood y by A5, FINTOPO7:def 1, A3;
then consider V being Element of the entourages of (Pervin_quasi_uniformity T) such that
A6: O = Neighborhood (V,y) ;
consider b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) such that
A7: b c= V by CARDFIL2:def 8;
FinMeetCl (subbasis_Pervin_quasi_uniformity T) c= <.(FinMeetCl (subbasis_Pervin_quasi_uniformity T)).] by CARDFIL2:18;
then A16: b in the entourages of (Pervin_quasi_uniformity T) ;
A17: [y,y] in id the carrier of (Pervin_quasi_uniformity T) by RELAT_1:def 10;
Pervin_quasi_uniformity T is axiom_U1 ;
then A18: id the carrier of (Pervin_quasi_uniformity T) c= b by A16;
reconsider B = { z where z is Element of the carrier of (Pervin_quasi_uniformity T) : [y,z] in b } as set ;
B c= the carrier of (Pervin_quasi_uniformity T)

proof

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

end;

then reconsider B = B as Subset of T ;

now :: thesis: ex B being Subset of T st
( B is open & B c= O1 & x in B )

take B = B; :: thesis: ( B is open & B c= O1 & x in B )
thus B is open by Th30, PRE_TOPC:def 2; :: thesis: ( B c= O1 & x in B )
B c= O

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B or t in O )
assume t in B ; :: thesis: t in O
then ex z being Element of T st
( t = z & [y,z] in b ) ;
hence t in O by A7, A6; :: thesis: verum

end;

hence B c= O1 ; :: thesis: x in B
thus x in B by A4, A18, A17; :: thesis: verum

end;

hence ex B being Subset of T st
( B is open & B c= O1 & x in B ) ; :: thesis: verum

end;

assume ex B being Subset of T st
( B is open & B c= O1 & x in B ) ; :: thesis: x in O1
hence x in O1 ; :: thesis: verum

end;

hence x in the topology of T by A2, PRE_TOPC:def 2, TOPS_1:25; :: thesis: verum

end;

the topology of T c= Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of T or x in Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T)) )
assume A20: x in the topology of T ; :: thesis: x in Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T))
then reconsider y = x as Subset of T ;
reconsider z = y as Subset of (Pervin_quasi_uniformity T) ;
for u being Element of (FMT_induced_by (Pervin_quasi_uniformity T)) st u in z holds
z in U_FMT u

proof

let u be Element of (FMT_induced_by (Pervin_quasi_uniformity T)); :: thesis: ( u in z implies z in U_FMT u )
assume A21: u in z ; :: thesis: z in U_FMT u
consider w being Element of the carrier of (Pervin_quasi_uniformity T) such that
A22: u = w and
A23: U_FMT u = Neighborhood w by Th31;
reconsider W = block_Pervin_quasi_uniformity y as Subset of [: the carrier of (Pervin_quasi_uniformity T), the carrier of (Pervin_quasi_uniformity T):] ;
A24: W in subbasis_Pervin_quasi_uniformity T by A20;
A25: subbasis_Pervin_quasi_uniformity T c= FinMeetCl (subbasis_Pervin_quasi_uniformity T) by CANTOR_1:4;
FinMeetCl (subbasis_Pervin_quasi_uniformity T) c= <.(FinMeetCl (subbasis_Pervin_quasi_uniformity T)).] by CARDFIL2:18;
then reconsider W = W as Element of the entourages of (Pervin_quasi_uniformity T) by A25, A24;
{ ww where ww is Element of T : [w,ww] in block_Pervin_quasi_uniformity y } = y

proof

thus { ww where ww is Element of T : [w,ww] in block_Pervin_quasi_uniformity y } c= y :: according to XBOOLE_0:def 10 :: thesis: y c= { ww where ww is Element of T : [w,ww] in block_Pervin_quasi_uniformity y }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ww where ww is Element of T : [w,ww] in block_Pervin_quasi_uniformity y } or a in y )
assume a in { ww where ww is Element of T : [w,ww] in block_Pervin_quasi_uniformity y } ; :: thesis: a in y
then consider ww being Element of T such that
A27: a = ww and
A28: [w,ww] in [:( the carrier of T \ y), the carrier of T:] \/ [: the carrier of T,y:] ;
( [w,ww] in [:( the carrier of T \ y), the carrier of T:] or [w,ww] in [: the carrier of T,y:] ) by A28, XBOOLE_0:def 3;
then ( ( w in the carrier of T \ y & ww in the carrier of T ) or ( w in the carrier of T & ww in y ) ) by ZFMISC_1:87;
hence a in y by A27, A21, A22, XBOOLE_0:def 5; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in y or a in { ww where ww is Element of T : [w,ww] in block_Pervin_quasi_uniformity y } )
assume A29: a in y ; :: thesis: a in { ww where ww is Element of T : [w,ww] in block_Pervin_quasi_uniformity y }
then reconsider b = a as Element of T ;
[w,b] in [: the carrier of T,y:] by A29, ZFMISC_1:87;
then [w,b] in block_Pervin_quasi_uniformity y by XBOOLE_0:def 3;
hence a in { ww where ww is Element of T : [w,ww] in block_Pervin_quasi_uniformity y } ; :: thesis: verum

end;

then z = Neighborhood (W,w) ;
hence z in U_FMT u by A23; :: thesis: verum

end;

then z is open Subset of (FMT_induced_by (Pervin_quasi_uniformity T)) by FINTOPO7:def 1;
hence x in Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T)) ; :: thesis: verum

end;

hence Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T)) = the topology of T by A1; :: thesis: verum