theorem Th66: :: TOPREAL6:68

for D being non empty bounded_below Subset of REAL holds lower_bound D = lower_bound (Cl D)