:: deftheorem Def6 defines diameter MEASURE5:def 6 :
for A being ext-real-membered set holds
( ( A <> {} implies diameter A = (sup A) - (inf A) ) & ( not A <> {} implies diameter A = 0. ) );