let X be TopSpace; :: thesis: for X1, X2 being SubSpace of X st X1 is SubSpace of X2 & X2 is SubSpace of X1 holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
let X1, X2 be SubSpace of X; :: thesis: ( X1 is SubSpace of X2 & X2 is SubSpace of X1 implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
set A1 = the carrier of X1;
set A2 = the carrier of X2;
assume ( X1 is SubSpace of X2 & X2 is SubSpace of X1 ) ; :: thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
then ( the carrier of X1 c= the carrier of X2 & the carrier of X2 c= the carrier of X1 ) by Th4;
then the carrier of X1 = the carrier of X2 by XBOOLE_0:def 10;
hence TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by Th5; :: thesis: verum