let C be Simple_closed_curve; :: thesis: (UMP C) `2 <= N-bound C
UMP C in C by Th30;
hence (UMP C) `2 <= N-bound C by PSCOMP_1:24; :: thesis: verum