theorem Th73: :: BORSUK_5:74

for X being compact Subset of R^1
for X9 being Subset of REAL
for x being Real st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )