let C be Simple_closed_curve; :: thesis: Lower_Middle_Point C <> Upper_Middle_Point C
(Lower_Middle_Point C) `2 <> (Upper_Middle_Point C) `2 by Th15;
hence Lower_Middle_Point C <> Upper_Middle_Point C ; :: thesis: verum