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;
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