let C be Simple_closed_curve; :: thesis: S-bound C < (UMP C) `2
set u = UMP C;
set l = LMP C;
UMP C in C by Th43;
then A1: S-bound C <= (UMP C) `2 by PSCOMP_1:71;

now

assume A2: S-bound C = (UMP C) `2 ; :: thesis: contradiction
A3: (LMP C) `2 < (UMP C) `2 by Th49;
LMP C in C by Th44;
hence contradiction by A2, A3, PSCOMP_1:71; :: thesis: verum

end;

hence S-bound C < (UMP C) `2 by A1, XXREAL_0:1; :: thesis: verum