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