theorem Th44: :: MEASURE6:44

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