for A being Interval
for x being Real holds diameter A = diameter (x ++ A)