theorem :: JORDAN16:1

for C being Simple_closed_curve holds Lower_Arc C <> Upper_Arc C