let I be Element of Family_of_Intervals ; :: thesis: ( not diameter I = +infty or sup I = +infty or inf I = -infty )
assume A1: diameter I = +infty ; :: thesis: ( sup I = +infty or inf I = -infty )
now :: thesis: ( sup I <> +infty implies not inf I <> -infty )
assume ( sup I <> +infty & inf I <> -infty ) ; :: thesis: contradiction
then (sup I) - (inf I) <> +infty by XXREAL_3:18;
hence contradiction by A1, MEASURE5:def 6; :: thesis: verum
end;
hence ( sup I = +infty or inf I = -infty ) ; :: thesis: verum