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