let S, T be TopStruct ; :: thesis: for B being Basis of S st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) holds
B is Basis of T
let B be Basis of S; :: thesis: ( TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) implies B is Basis of T )
assume A1: TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) ; :: thesis: B is Basis of T
then A2: the topology of T c= UniCl B by CANTOR_1:def 2;
B c= the topology of S by CANTOR_1:def 2;
hence B is Basis of T by A1, A2, CANTOR_1:def 2; :: thesis: verum