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: LMP C in South_Arc C by Th34;
A2: North_Arc C c= C by Th35;
A3: UMP C in North_Arc C by Th33;
A4: South_Arc C c= C by Th36;

now :: thesis: ( ( LE LMP C, UMP C,C & UMP C in Lower_Arc C & LMP C in Upper_Arc C ) or ( LE UMP C, LMP C,C & LMP C in Lower_Arc C & UMP C in Upper_Arc C ) )

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

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:49, JORDAN21:50; :: 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:49, JORDAN21:50; :: 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