theorem Th25: :: YELLOW14:25

for S, T being TopStruct
for A being Subset of S
for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact holds
B is compact