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 )
assume A1: 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 A2: B c= the topology of T by CANTOR_1:def 5;
consider F being Basis of S such that
A3: F c= FinMeetCl B by CANTOR_1:def 5;
F is Basis of T by A1, Th32;
hence B is prebasis of T by A1, A2, A3, CANTOR_1:def 5; :: thesis: verum