:: deftheorem Def5 defines diameter JORDAN_A:def 5 :
for n being Nat
for C being Subset of (TOP-REAL n)
for b₃ being Real holds
( b₃ = diameter C iff ex W being Subset of (Euclid n) st
( W = C & b₃ = diameter W ) );