let C be Simple_closed_curve; :: thesis: for p, q being Point of (TOP-REAL 2) st p in C & q in C & not LE p,q,C holds
LE q,p,C
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in C & q in C & not LE p,q,C implies LE q,p,C )
assume that
A1: p in C and
A2: q in C ; :: thesis: ( LE p,q,C or LE q,p,C )
A3: C = (Lower_Arc C) \/ (Upper_Arc C) by JORDAN6:50;
per cases ( p = q or ( p in Lower_Arc C & p <> W-min C & q in Lower_Arc C & q <> W-min C & p <> q ) or ( p in Lower_Arc C & p <> W-min C & q in Upper_Arc C ) or ( p in Upper_Arc C & q in Lower_Arc C & q <> W-min C ) or ( p in Upper_Arc C & q in Upper_Arc C & p <> q ) ) by A1, A2, A3, JORDAN7:1, XBOOLE_0:def 3;
suppose p = q ; :: thesis: ( LE p,q,C or LE q,p,C )
hence ( LE p,q,C or LE q,p,C ) by A1, JORDAN6:56; :: thesis: verum
end;
suppose that A4: ( p in Lower_Arc C & p <> W-min C & q in Lower_Arc C & q <> W-min C ) and
A5: p <> q ; :: thesis: ( LE p,q,C or LE q,p,C )
Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
then ( LE p,q, Lower_Arc C, E-max C, W-min C or LE q,p, Lower_Arc C, E-max C, W-min C ) by A4, A5, JORDAN5C:14;
hence ( LE p,q,C or LE q,p,C ) by A4, JORDAN6:def 10; :: thesis: verum
end;
suppose ( p in Lower_Arc C & p <> W-min C & q in Upper_Arc C ) ; :: thesis: ( LE p,q,C or LE q,p,C )
hence ( LE p,q,C or LE q,p,C ) by JORDAN6:def 10; :: thesis: verum
end;
suppose ( p in Upper_Arc C & q in Lower_Arc C & q <> W-min C ) ; :: thesis: ( LE p,q,C or LE q,p,C )
hence ( LE p,q,C or LE q,p,C ) by JORDAN6:def 10; :: thesis: verum
end;
suppose that A6: ( p in Upper_Arc C & q in Upper_Arc C ) and
A7: p <> q ; :: thesis: ( LE p,q,C or LE q,p,C )
Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
then ( LE p,q, Upper_Arc C, W-min C, E-max C or LE q,p, Upper_Arc C, W-min C, E-max C ) by A6, A7, JORDAN5C:14;
hence ( LE p,q,C or LE q,p,C ) by A6, JORDAN6:def 10; :: thesis: verum
end;
end;