let p1, p2 be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & not LE p1,p2,P holds
LE p2,p1,P
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & p1 in P & p2 in P & not LE p1,p2,P implies LE p2,p1,P )
assume A1: ( P is being_simple_closed_curve & p1 in P & p2 in P & not LE p1,p2,P ) ; :: thesis: LE p2,p1,P
then A2: P = (Upper_Arc P) \/ (Lower_Arc P) by JORDAN6:def 9;
A3: not p1 = W-min P by A1, JORDAN7:3;
per cases ( ( p1 in Upper_Arc P & p2 in Upper_Arc P ) or ( p1 in Upper_Arc P & p2 in Lower_Arc P ) or ( p1 in Lower_Arc P & p2 in Upper_Arc P ) or ( p1 in Lower_Arc P & p2 in Lower_Arc P ) ) by A1, A2, XBOOLE_0:def 3;
suppose A4: ( p1 in Upper_Arc P & p2 in Upper_Arc P ) ; :: thesis: LE p2,p1,P
A5: 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
per cases ( p1 <> p2 or p1 = p2 ) ;
case A6: p1 <> p2 ; :: thesis: LE p2,p1,P
now
per cases ( ( 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 ) or ( 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 ) ) by A4, A5, A6, 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: contradiction
hence contradiction by A1, A4, JORDAN6:def 10; :: thesis: verum
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: LE p2,p1,P
hence LE p2,p1,P by A4, JORDAN6:def 10; :: thesis: verum
end;
end;
end;
hence LE p2,p1,P ; :: thesis: verum
end;
case p1 = p2 ; :: thesis: LE p2,p1,P
hence LE p2,p1,P by A1, JORDAN6:71; :: thesis: verum
end;
end;
end;
hence LE p2,p1,P ; :: thesis: verum
end;
suppose A7: ( p1 in Upper_Arc P & p2 in Lower_Arc P ) ; :: thesis: LE p2,p1,P
hence LE p2,p1,P ; :: thesis: verum
end;
suppose ( p1 in Lower_Arc P & p2 in Upper_Arc P ) ; :: thesis: LE p2,p1,P
hence LE p2,p1,P by A3, JORDAN6:def 10; :: thesis: verum
end;
suppose A8: ( p1 in Lower_Arc P & p2 in Lower_Arc P ) ; :: thesis: LE p2,p1,P
A9: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, JORDAN6:65;
set q2 = W-min P;
set q1 = E-max P;
set Q = Lower_Arc P;
now
per cases ( p1 <> p2 or p1 = p2 ) ;
case A10: p1 <> p2 ; :: thesis: LE p2,p1,P
now
per cases ( ( 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 ) or ( 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 ) ) by A8, A9, A10, JORDAN5C:14;
case A11: ( 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: LE p2,p1,P
hence LE p2,p1,P ; :: thesis: verum
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: LE p2,p1,P
hence LE p2,p1,P by A3, A8, JORDAN6:def 10; :: thesis: verum
end;
end;
end;
hence LE p2,p1,P ; :: thesis: verum
end;
case p1 = p2 ; :: thesis: LE p2,p1,P
hence LE p2,p1,P by A1, JORDAN6:71; :: thesis: verum
end;
end;
end;
hence LE p2,p1,P ; :: thesis: verum
end;
end;