theorem Th8: :: COMPTS_1:8

for T being TopStruct
for P being Subset of T st T is compact & P is closed holds
P is compact