theorem Th15: :: JORDAN21:15

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