theorem Th26: :: MEASURE6:26
for A being Interval
for x being Real holds
( A is open_interval iff x ++ A is open_interval )