theorem Th2: :: INTEGRA1:4

for A being non empty closed_interval Subset of REAL holds A = [.(lower_bound A),(upper_bound A).]