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 )
A1: B c= the topology of S by TOPS_2:64;
assume A2: 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 the topology of T c= UniCl B by CANTOR_1:def 2;
hence B is Basis of T by A2, A1, CANTOR_1:def 2, TOPS_2:64; :: thesis: verum