theorem Th29: :: MEASURE6:29

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