for C being Simple_closed_curve holds (Lower_Middle_Point C) `2 <> (Upper_Middle_Point C) `2