theorem :: JORDAN21:48

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