for C being Simple_closed_curve holds S-bound C <= (LMP (Lower_Arc C)) `2