let A be Interval; :: thesis: for a, b being R_eal st a = -infty & b = +infty & ( A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.] ) holds
diameter A = +infty
let a, b be R_eal; :: thesis: ( a = -infty & b = +infty & ( A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.] ) implies diameter A = +infty )
assume A1: ( a = -infty & b = +infty & ( A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.] ) ) ; :: thesis: diameter A = +infty
B: ( sup A = +infty & inf A = -infty ) by A1, XXREAL_2:25, XXREAL_2:26, XXREAL_2:27, XXREAL_2:28, XXREAL_2:29, XXREAL_2:30, XXREAL_2:31, XXREAL_2:32;
then not A is empty by XXREAL_2:40;
then diameter A = b - a by Def10, A1, B
.= +infty by A1, XXREAL_3:13 ;
hence diameter A = +infty ; :: thesis: verum