let C be Simple_closed_curve; :: thesis: S-bound C <= (LMP C) `2
LMP C in C by Th31;
hence S-bound C <= (LMP C) `2 by PSCOMP_1:24; :: thesis: verum