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 A1: ( the carrier of T1 = the carrier of T2 & B is Basis of T2 ) ; :: thesis: the topology of T1 = the topology of T2
then reconsider C = B as Basis of T2 ;
thus the topology of T1 = UniCl C by A1, Th22
.= the topology of T2 by Th22 ; :: thesis: verum