theorem Th67: :: TOPREAL6:69

for D being non empty bounded_above Subset of REAL holds upper_bound D = upper_bound (Cl D)