let p1, p2 be Point of (TOP-REAL 2); :: thesis:
let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
assume that
A1: P is being_simple_closed_curve and
A2: p1 in P and
A3: p2 in P and
A4: not LE p1,p2,P ; :: thesis:
A5: P = (Upper_Arc P) \/ (Lower_Arc P) by A1, JORDAN6:def 9;
A6: not p1 = W-min P by A1, A3, A4, JORDAN7:3;

per cases by A2, A3, A5, XBOOLE_0:def 3;

suppose A7: ( p1 in Upper_Arc P & p2 in Upper_Arc P ) ; :: thesis:

A8: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, JORDAN6:def 8;
set q1 = W-min P;
set q2 = E-max P;
set Q = Upper_Arc P;

now :: thesis:

per cases ;

case A9: p1 <> p2 ; :: thesis:

now :: thesis:

per cases by A7, A8, A9, JORDAN5C:14;

case ( LE p1,p2, Upper_Arc P, W-min P, E-max P & not LE p2,p1, Upper_Arc P, W-min P, E-max P ) ; :: thesis:

hence contradiction by A4, A7, JORDAN6:def 10; :: thesis:

end;

case ( LE p2,p1, Upper_Arc P, W-min P, E-max P & not LE p1,p2, Upper_Arc P, W-min P, E-max P ) ; :: thesis:

hence LE p2,p1,P by A7, JORDAN6:def 10; :: thesis:

end;

end;

end;

hence LE p2,p1,P ; :: thesis:

end;

case p1 = p2 ; :: thesis:

hence LE p2,p1,P by A1, A2, JORDAN6:56; :: thesis:

end;

end;

end;

hence LE p2,p1,P ; :: thesis:

end;

suppose A10: ( p1 in Upper_Arc P & p2 in Lower_Arc P ) ; :: thesis:

now :: thesis:

per cases ;

case p2 = W-min P ; :: thesis:

hence LE p2,p1,P by A1, A2, JORDAN7:3; :: thesis:

end;

case p2 <> W-min P ; :: thesis:

hence contradiction by A4, A10, JORDAN6:def 10; :: thesis:

end;

end;

end;

hence LE p2,p1,P ; :: thesis:

end;

suppose ( p1 in Lower_Arc P & p2 in Upper_Arc P ) ; :: thesis:

hence LE p2,p1,P by A6, JORDAN6:def 10; :: thesis:

end;

suppose A11: ( p1 in Lower_Arc P & p2 in Lower_Arc P ) ; :: thesis:

A12: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, JORDAN6:50;
set q2 = W-min P;
set q1 = E-max P;
set Q = Lower_Arc P;

now :: thesis:

per cases ;

case A13: p1 <> p2 ; :: thesis:

now :: thesis:

per cases by A11, A12, A13, JORDAN5C:14;

case A14: ( LE p1,p2, Lower_Arc P, E-max P, W-min P & not LE p2,p1, Lower_Arc P, E-max P, W-min P ) ; :: thesis:

now :: thesis:

per cases ;

case p2 = W-min P ; :: thesis:

hence LE p2,p1,P by A1, A2, JORDAN7:3; :: thesis:

end;

case p2 <> W-min P ; :: thesis:

hence contradiction by A4, A11, A14, JORDAN6:def 10; :: thesis:

end;

end;

end;

hence LE p2,p1,P ; :: thesis:

end;

case ( LE p2,p1, Lower_Arc P, E-max P, W-min P & not LE p1,p2, Lower_Arc P, E-max P, W-min P ) ; :: thesis:

hence LE p2,p1,P by A6, A11, JORDAN6:def 10; :: thesis:

end;

end;

end;

hence LE p2,p1,P ; :: thesis:

end;

case p1 = p2 ; :: thesis:

hence LE p2,p1,P by A1, A2, JORDAN6:56; :: thesis:

end;

end;

end;

hence LE p2,p1,P ; :: thesis:

end;

end;