theorem Th47: :: COUSIN2:54

for I being non empty closed_interval Subset of REAL
for D being Division of I st divset (D,1) = [.(D . 1),(D . 1).] holds
D . 1 = lower_bound I