theorem Th43: :: MEASURE6:43

for X being non empty Subset of REAL st X is bounded_below holds
lower_bound X = - (upper_bound (-- X))