theorem Th5: :: TSEP_1:5

for X being TopStruct
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 #)