theorem Th17: :: RCOMP_3:17

for X being real-bounded interval Subset of REAL st lower_bound X in X & not upper_bound X in X holds
X = [.(lower_bound X),(upper_bound X).[