let T1, T2 be TopSpace; :: thesis: for B being Basis of T1 st the carrier of T1 = the carrier of T2 & B is Basis of T2 holds
the topology of T1 = the topology of T2
let B be Basis of T1; :: thesis: ( the carrier of T1 = the carrier of T2 & B is Basis of T2 implies the topology of T1 = the topology of T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: B is Basis of T2 ; :: thesis: the topology of T1 = the topology of T2
reconsider C = B as Basis of T2 by A2;
thus the topology of T1 = UniCl C by A1, Th22
.= the topology of T2 by Th22 ; :: thesis: verum