for C being Simple_closed_curve
for S being Segmentation of C
for i being Nat holds diameter (Segm (S,i)) <= diameter S