theorem :: TSEP_1:93

for T being TopStruct holds T | ([#] T) = TopStruct(# the carrier of T, the topology of T #)