let T1, T2 be non empty strict TopSpace; :: thesis: for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds
T1 = T2
let P be prebasis of T1; :: thesis: ( the carrier of T1 = the carrier of T2 & P is prebasis of T2 implies T1 = T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: P is prebasis of T2 ; :: thesis: T1 = T2
reconsider P9 = P as prebasis of T2 by A2;
consider B1 being Basis of T1 such that
A3: B1 c= FinMeetCl P by Def4;
P c= the topology of T1 by TOPS_2:64;
then FinMeetCl P c= FinMeetCl the topology of T1 by Th14;
then A4: UniCl (FinMeetCl P) c= UniCl (FinMeetCl the topology of T1) by Th9;
P9 c= the topology of T2 by TOPS_2:64;
then FinMeetCl P9 c= FinMeetCl the topology of T2 by Th14;
then A5: UniCl (FinMeetCl P9) c= UniCl (FinMeetCl the topology of T2) by Th9;
A6: the topology of T1 c= UniCl B1 by Def2;
UniCl B1 c= UniCl (FinMeetCl P) by A3, Th9;
then A7: the topology of T1 c= UniCl (FinMeetCl P) by A6;
consider B2 being Basis of T2 such that
A8: B2 c= FinMeetCl P9 by Def4;
A9: the topology of T2 c= UniCl B2 by Def2;
UniCl B2 c= UniCl (FinMeetCl P9) by A8, Th9;
then A10: the topology of T2 c= UniCl (FinMeetCl P9) by A9;
the topology of T2 = UniCl (FinMeetCl the topology of T2) by Th7;
then A11: UniCl (FinMeetCl P9) = the topology of T2 by A10, A5;
the topology of T1 = UniCl (FinMeetCl the topology of T1) by Th7;
hence T1 = T2 by A1, A7, A11, A4, XBOOLE_0:def 10; :: thesis: verum