theorem :: MEASURE6:21

for A, B being real-membered set
for y being Real holds
( y in B ++ A iff ex x, z being Real st
( x in B & z in A & y = x + z ) )