theorem :: JORDAN21:16

for C being Simple_closed_curve holds Lower_Middle_Point C <> Upper_Middle_Point C