theorem Th19: :: RCOMP_3:19

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