theorem :: MEASURE6:25

for x being Real holds x ++ {} = {} ;