let C be Simple_closed_curve; :: thesis: S-bound C < (UMP C) `2
set u = UMP C;
set l = LMP C;

A1: now :: thesis: not S-bound C = (UMP C) `2

assume A2: S-bound C = (UMP C) `2 ; :: thesis: contradiction
( (LMP C) `2 < (UMP C) `2 & LMP C in C ) by Th31, Th36;
hence contradiction by A2, PSCOMP_1:24; :: thesis: verum

end;

UMP C in C by Th30;
then S-bound C <= (UMP C) `2 by PSCOMP_1:24;
hence S-bound C < (UMP C) `2 by A1, XXREAL_0:1; :: thesis: verum