let C be Simple_closed_curve; :: thesis: (LMP C) `2 < N-bound C
set u = UMP C;
set l = LMP C;
A1: now :: thesis: not N-bound C = (LMP C) `2
assume A2: N-bound C = (LMP C) `2 ; :: thesis: contradiction
( (LMP C) `2 < (UMP C) `2 & UMP C in C ) by Th30, Th36;
hence contradiction by A2, PSCOMP_1:24; :: thesis: verum
end;
LMP C in C by Th31;
then (LMP C) `2 <= N-bound C by PSCOMP_1:24;
hence (LMP C) `2 < N-bound C by A1, XXREAL_0:1; :: thesis: verum