let A be Interval; :: thesis: for x being real number holds diameter A = diameter (x ++ A)
let x be real number ; :: thesis: diameter A = diameter (x ++ A)

per cases ( A is empty or not A is empty ) ;

suppose A1: A is empty ; :: thesis: diameter A = diameter (x ++ A)

now

assume not x ++ A is empty ; :: thesis: contradiction
then consider y being real number such that
A2: y in x ++ A by MEMBERED:9;
reconsider y = y as Real by XREAL_0:def 1;
ex z being Real st
( z in A & y = x + z ) by A2, Def6;
hence contradiction by A1; :: thesis: verum

end;

hence diameter A = diameter (x ++ A) by A1; :: thesis: verum

end;

suppose A3: not A is empty ; :: thesis: diameter A = diameter (x ++ A)

then consider y being real number such that
A4: y in A by MEMBERED:9;
reconsider y = y as Real by XREAL_0:def 1;
A5: x + y in x ++ A by A4, Def6;
reconsider y = x as R_eal by XXREAL_0:def 1;
thus diameter A = (sup A) - (inf A) by A3, MEASURE5:def 10
.= (y + (sup A)) - (y + (inf A)) by XXREAL_3:34
.= (sup (x ++ A)) - (y + (inf A)) by Th67
.= (sup (x ++ A)) - (inf (x ++ A)) by Th68
.= diameter (x ++ A) by A5, MEASURE5:def 10 ; :: thesis: verum

end;

end;