let T1, T2 be TopSpace; :: thesis: for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds
the topology of T1 = the topology of T2
let P be prebasis of T1; :: thesis: ( the carrier of T1 = the carrier of T2 & P is prebasis of T2 implies the topology of T1 = the topology of T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: P is prebasis of T2 ; :: thesis: the topology of T1 = the topology of T2
reconsider C = P as prebasis of T2 by A2;
A3: FinMeetCl P is Basis of T1 by Th23;
FinMeetCl C is Basis of T2 by Th23;
hence the topology of T1 = the topology of T2 by A1, A3, Th25; :: thesis: verum