theorem :: RCOMP_1:11

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