theorem Th27: :: MEASURE6:27

for A being Interval
for x being Real holds
( A is closed_interval iff x ++ A is closed_interval )