now :: thesis:

thus the carrier of (TopSpace_induced_by (@ (uniformity_induced_by R))) = the carrier of (partition_topology (Class R)) by FINTOPO7:def 16; :: thesis:
A1: the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) = Family_open_set (FMT_induced_by (@ (uniformity_induced_by R))) by FINTOPO7:def 16
.= { O where O is open Subset of (FMT_induced_by (@ (uniformity_induced_by R))) : verum } ;
A2: the topology of (partition_topology (Class R)) = { (union P) where P is Subset of (Class R) : verum } by Th14;
A3: the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) c= the topology of (partition_topology (Class R))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) ; :: thesis:
then consider O being open Subset of (FMT_induced_by (@ (uniformity_induced_by R))) such that
A4: t = O by A1;

per cases ;

suppose A5: O is empty ; :: thesis:

{} c= Class R ;
then reconsider P = {} as Subset of (Class R) ;
t = union P by A4, A5, ZFMISC_1:2;
hence t in the topology of (partition_topology (Class R)) by A2; :: thesis:

end;

suppose A6: not O is empty ; :: thesis:

set P = { (Class (R,u)) where u is Element of O : verum } ;
{ (Class (R,u)) where u is Element of O : verum } c= Class R

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in { (Class (R,u)) where u is Element of O : verum } ; :: thesis:
then consider u0 being Element of O such that
A7: u = Class (R,u0) ;
A8: u0 in O by A6;
thus u in Class R by A7, A8, EQREL_1:def 3; :: thesis:

end;

then reconsider P = { (Class (R,u)) where u is Element of O : verum } as Subset of (Class R) ;
reconsider t1 = t as Subset of X by A4;
t1 = union P

proof

thus t1 c= union P :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: a in t1 ; :: thesis:
then reconsider b = a as Element of O by A4;
( b in Class (R,b) & Class (R,b) in P ) by A10, EQREL_1:20;
hence a in union P by TARSKI:def 4; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in union P ; :: thesis:
then consider Q being set such that
A11: a in Q and
A12: Q in P by TARSKI:def 4;
consider v being Element of O such that
A13: Q = Class (R,v) by A12;
v in O by A6;
then reconsider w = v as Element of (@ (uniformity_induced_by R)) ;
O in Neighborhood w by Th8, A6;
then consider V being Element of the entourages of (@ (uniformity_induced_by R)) such that
A14: O = Neighborhood (V,w) ;
V in rho R ;
then consider W being Relation of the carrier of (@ (uniformity_induced_by R)) such that
A15: V = W and
A16: R c= W ;
A17: ( Neighborhood (V,w) = V .: {w} & Neighborhood (V,w) = rng (V | {w}) & Neighborhood (V,w) = Im (V,w) & Neighborhood (V,w) = Class (V,w) & Neighborhood (V,w) = neighbourhood (,) ) by UNIFORM2:14;
Class (R,w) c= Class (W,w)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in Class (R,w) ; :: thesis:
then [w,z] in W by A16, EQREL_1:18;
hence z in Class (W,w) by EQREL_1:18; :: thesis:

end;

hence a in t1 by A11, A13, A4, A17, A15, A14; :: thesis:

end;

hence t in the topology of (partition_topology (Class R)) by A2; :: thesis:

end;

the topology of (partition_topology (Class R)) c= the topology of (TopSpace_induced_by (@ (uniformity_induced_by R)))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A18: t in the topology of (partition_topology (Class R)) ; :: thesis:
then consider P being Subset of (Class R) such that
A19: t = union P by A2;
reconsider Q = union P as Subset of (FMT_induced_by (@ (uniformity_induced_by R))) by A18, A19;
for x being Element of (@ (uniformity_induced_by R)) st x in Q holds
Q in Neighborhood x

proof

let x be Element of (@ (uniformity_induced_by R)); :: thesis:
assume A20: x in Q ; :: thesis:
then consider T being set such that
A21: x in T and
A22: T in P by TARSKI:def 4;
T in Class R by A22;
then consider b being object such that
A23: b in X and
A24: T = Class (R,b) by EQREL_1:def 3;
set S1 = { [x,y] where y is Element of Q : verum } ;
set S = R \/ { [x,y] where y is Element of Q : verum } ;
{ [x,y] where y is Element of Q : verum } c= [:X,X:]

proof

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume s in { [x,y] where y is Element of Q : verum } ; :: thesis:
then consider y being Element of Q such that
A25: s = [x,y] ;
Q c= X ;
then y in X by A20;
hence s in [:X,X:] by A25, ZFMISC_1:def 2; :: thesis:

end;

then reconsider S = R \/ { [x,y] where y is Element of Q : verum } as Subset of [:X,X:] by XBOOLE_1:8;
R c= S by XBOOLE_1:7;
then S in rho R ;
then reconsider V = S as Element of the entourages of (@ (uniformity_induced_by R)) ;
Q = Neighborhood (V,x)

proof

thus Q c= Neighborhood (V,x) :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in Q ; :: thesis:
then reconsider b = a as Element of Q ;
A27: [x,b] in { [x,y] where y is Element of Q : verum } ;
A28: { [x,y] where y is Element of Q : verum } c= R \/ { [x,y] where y is Element of Q : verum } by XBOOLE_1:7;
b in Q by A20;
then reconsider c = b as Element of (@ (uniformity_induced_by R)) ;
[x,c] in V by A28, A27;
hence a in Neighborhood (V,x) ; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in Neighborhood (V,x) ; :: thesis:
then consider y being Element of (@ (uniformity_induced_by R)) such that
A29: a = y and
A30: [x,y] in V ;

per cases in { [x,y] where y is Element of Q : verum } or [x,a] in R ) by A29, A30, XBOOLE_0:def 3;

suppose [x,a] in { [x,y] where y is Element of Q : verum } ; :: thesis:

then consider y being Element of Q such that
A31: [x,a] = [x,y] ;
a = y by A31, XTUPLE_0:1;
hence a in Q by A20; :: thesis:

end;

suppose [x,a] in R ; :: thesis:

then A32: a in Class (R,x) by EQREL_1:18;
Class (R,b) = Class (R,x) by A21, A23, A24, EQREL_1:23;
hence a in Q by A22, A24, A32, TARSKI:def 4; :: thesis:

end;

hence Q in Neighborhood x ; :: thesis:

end;

then reconsider O = union P as open Subset of (FMT_induced_by (@ (uniformity_induced_by R))) by Th8;
t = O by A19;
hence t in the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) by A1; :: thesis:

end;

hence the topology of (TopSpace_induced_by (@ (uniformity_induced_by R))) = the topology of (partition_topology (Class R)) by A3; :: thesis:

end;