theorem Th31: :: MEASURE6:31

for A being real-membered set
for x being Real
for y being R_eal st x = y holds
sup (x ++ A) = y + (sup A)