:: deftheorem Def2 defines diameter COMPL_SP:def 2 :
for M being non empty Reflexive MetrStruct
for S being SetSequence of M
for b₃ being Real_Sequence holds
( b₃ = diameter S iff for i being Nat holds b₃ . i = diameter (S . i) );