theorem Th23: :: BORSUK_4:26

for X being Subset of I[01]
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 )