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

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

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

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

end;

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

then consider y being Real such that
A2: y in A ;
reconsider y = y as Real ;
A3: x + y in x ++ A by A2, Lm1;
reconsider y = x as R_eal by XXREAL_0:def 1;
thus diameter A = (sup A) - (inf A) by A1, MEASURE5:def 6
.= (y + (sup A)) - (y + (inf A)) by XXREAL_3:33
.= (sup (x ++ A)) - (y + (inf A)) by Th31
.= (sup (x ++ A)) - (inf (x ++ A)) by Th32
.= diameter (x ++ A) by A3, MEASURE5:def 6 ; :: thesis: verum

end;

end;