theorem Th10: :: RCOMP_1:10

for X being Subset of REAL st X is compact holds
X is real-bounded