for C being Simple_closed_curve
for e being Real st e > 0 holds
ex S being Segmentation of C st diameter S < e