theorem Th8: :: RCOMP_1:8

for X being Subset of REAL st X is compact holds
X is closed