let C be Simple_closed_curve; :: thesis: UMP C <> LMP C
assume A1: UMP C = LMP C ; :: thesis: contradiction
(LMP C) `2 < (UMP C) `2 by Th36;
hence contradiction by A1; :: thesis: verum