let X be TopStruct ; :: thesis: for X1, X2 being SubSpace of X st the carrier of X1 = the carrier of X2 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: ( the carrier of X1 = the carrier of X2 implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
reconsider S1 = TopStruct(# the carrier of X1, the topology of X1 #), S2 = TopStruct(# the carrier of X2, the topology of X2 #) as strict SubSpace of X by Lm3;
set A1 = the carrier of X1;
set A2 = the carrier of X2;
assume A1: the carrier of X1 = the carrier of X2 ; :: thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
A2: the carrier of X1 = [#] S1 ;
A3: the carrier of X2 = [#] S2 ;
reconsider A1 = the carrier of X1 as Subset of X by BORSUK_1:1;
S1 = X | A1 by A2, PRE_TOPC:def 5;
hence TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, A3, PRE_TOPC:def 5; :: thesis: verum