let A be Interval; 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; ( 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.] )
; 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
; verum