let C be Simple_closed_curve; :: thesis: ( ( 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 ) )
A1: South_Arc C c= C by Th38;
A2: LMP C in South_Arc C by Th36;
A3: North_Arc C c= C by Th37;
A4: UMP C in North_Arc C by Th35;

now

per cases ( LE LMP C, UMP C,C or LE UMP C, LMP C,C ) by A1, A2, A3, A4, JORDAN16:11;

case LE LMP C, UMP C,C ; :: thesis: ( UMP C in Lower_Arc C & LMP C in Upper_Arc C )

then ( ( LMP C in Upper_Arc C & UMP C in Lower_Arc C ) or ( LMP C in Lower_Arc C & UMP C in Lower_Arc C ) or ( LMP C in Upper_Arc C & UMP C in Upper_Arc C ) ) by JORDAN6:def 10;
hence ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) by JORDAN21:62, JORDAN21:63; :: thesis: verum

end;

case LE UMP C, LMP C,C ; :: thesis: ( LMP C in Lower_Arc C & UMP C in Upper_Arc C )

then ( ( UMP C in Upper_Arc C & LMP C in Lower_Arc C ) or ( LMP C in Lower_Arc C & UMP C in Lower_Arc C ) or ( LMP C in Upper_Arc C & UMP C in Upper_Arc C ) ) by JORDAN6:def 10;
hence ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) by JORDAN21:62, JORDAN21:63; :: thesis: verum

end;

end;

end;

hence ( ( 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 ) ) ; :: thesis: verum