:: deftheorem Def8 defines diameter TBSP_1:def 8 :
for N being non empty Reflexive MetrStruct
for C being Subset of N st C is bounded holds
for b₃ being Real holds
( ( C <> {} implies ( b₃ = diameter C iff ( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= b₃ ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
b₃ <= s ) ) ) ) & ( not C <> {} implies ( b₃ = diameter C iff b₃ = 0 ) ) );