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 that

A1: ( a = -infty & b = +infty ) and

A2: ( A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.] ) ; :: thesis: diameter A = +infty

A3: ( sup A = +infty & inf A = -infty ) by A1, A2, 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 A1, A3, Def6

.= +infty by A1, XXREAL_3:13 ;

hence diameter A = +infty ; :: thesis: verum

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 that

A1: ( a = -infty & b = +infty ) and

A2: ( A = ].a,b.[ or A = [.a,b.] or A = [.a,b.[ or A = ].a,b.] ) ; :: thesis: diameter A = +infty

A3: ( sup A = +infty & inf A = -infty ) by A1, A2, 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 A1, A3, Def6

.= +infty by A1, XXREAL_3:13 ;

hence diameter A = +infty ; :: thesis: verum