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