for C being Simple_closed_curve holds
( ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) or ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) )