theorem Th32: :: MEASURE6:32

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