let S, T be TopStruct ; :: thesis: for B being prebasis of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds
B is prebasis of T
let B be prebasis of S; :: thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) implies B is prebasis of T )
consider F being Basis of S such that
A1: F c= FinMeetCl B by CANTOR_1:def 4;
assume A2: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; :: thesis: B is prebasis of T
then ( B c= the topology of T & F is Basis of T ) by Th32, TOPS_2:64;
hence B is prebasis of T by A2, A1, CANTOR_1:def 4, TOPS_2:64; :: thesis: verum