theorem :: COMPTS_1:23

for T being non empty TopSpace
for X being set holds
( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) )