theorem Th13: :: RCOMP_3:13

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