let P be Subset of (TOP-REAL 2); :: thesis:
let q1, q2 be Point of (TOP-REAL 2); :: thesis:
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q1,P ; :: thesis:
A4: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, Def9;
A5: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A1, Def9;
A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50;

now :: thesis:

per cases by A2;

case A7: ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) ; :: thesis:

now :: thesis:

per cases by A3;

case A8: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; :: thesis:

then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def 4;
then A9: q1 = E-max P by A5, A8, TARSKI:def 2;
q2 in (Upper_Arc P) /\ (Lower_Arc P) by A7, A8, XBOOLE_0:def 4;
hence q1 = q2 by A5, A7, A9, TARSKI:def 2; :: thesis:

end;

case A10: ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; :: thesis:

then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def 4;
then q2 = E-max P by A5, A7, TARSKI:def 2;
hence q1 = q2 by A6, A10, Th55; :: thesis:

end;

case A11: ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; :: thesis:

then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def 4;
then q1 = E-max P by A5, A11, TARSKI:def 2;
hence q1 = q2 by A4, A11, Th54; :: thesis:

end;

end;

end;

hence q1 = q2 ; :: thesis:

end;

case A12: ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) ; :: thesis:

now :: thesis:

per cases by A3;

case A13: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; :: thesis:

then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A12, XBOOLE_0:def 4;
then q1 = E-max P by A5, A13, TARSKI:def 2;
hence q1 = q2 by A6, A12, Th55; :: thesis:

end;

case ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; :: thesis:

hence q1 = q2 by A6, A12, JORDAN5C:12; :: thesis:

end;

case A14: ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; :: thesis:

then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A12, XBOOLE_0:def 4;
then q1 = E-max P by A5, A14, TARSKI:def 2;
hence q1 = q2 by A4, A14, Th54; :: thesis:

end;

end;

end;

hence q1 = q2 ; :: thesis:

end;

case A15: ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ; :: thesis:

now :: thesis:

per cases by A3;

case ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; :: thesis:

then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A15, XBOOLE_0:def 4;
then q2 = E-max P by A5, A15, TARSKI:def 2;
hence q1 = q2 by A4, A15, Th54; :: thesis:

end;

case A16: ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; :: thesis:

then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A15, XBOOLE_0:def 4;
then q2 = E-max P by A5, A15, TARSKI:def 2;
hence q1 = q2 by A6, A16, Th55; :: thesis:

end;

case ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; :: thesis:

hence q1 = q2 by A4, A15, JORDAN5C:12; :: thesis:

end;

end;

end;

hence q1 = q2 ; :: thesis:

end;

end;

end;

hence q1 = q2 ; :: thesis: