let p1, p2 be Point of (); :: thesis: for P being non empty compact Subset of () 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 (); :: thesis: ( P is being_simple_closed_curve & p1 in P & p2 in P & not LE p1,p2,P implies LE p2,p1,P )
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: LE p2,p1,P
A5: P = () \/ () by ;
A6: not p1 = W-min P by ;
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 ;
suppose A7: ( p1 in Upper_Arc P & p2 in Upper_Arc P ) ; :: thesis: LE p2,p1,P
A8: Upper_Arc P is_an_arc_of W-min P, E-max P by ;
set q1 = W-min P;
set q2 = E-max P;
set Q = Upper_Arc P;
now :: thesis: ( ( p1 <> p2 & LE p2,p1,P ) or ( p1 = p2 & LE p2,p1,P ) )
per cases ( p1 <> p2 or p1 = p2 ) ;
case A9: p1 <> p2 ; :: thesis: LE p2,p1,P
now :: thesis: ( ( 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 & contradiction ) 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 & LE p2,p1,P ) )
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 ;
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
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 ; :: 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 ; :: thesis: verum
end;
end;
end;
hence LE p2,p1,P ; :: thesis: verum
end;
suppose A10: ( p1 in Upper_Arc P & p2 in Lower_Arc P ) ; :: thesis: LE p2,p1,P
now :: thesis: ( ( p2 = W-min P & LE p2,p1,P ) or ( p2 <> W-min P & contradiction ) )
per cases ( p2 = W-min P or p2 <> W-min P ) ;
case p2 = W-min P ; :: thesis: LE p2,p1,P
hence LE p2,p1,P by ; :: thesis: verum
end;
end;
end;
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 ; :: thesis: verum
end;
suppose A11: ( p1 in Lower_Arc P & p2 in Lower_Arc P ) ; :: thesis: LE p2,p1,P
A12: Lower_Arc P is_an_arc_of E-max P, W-min P by ;
set q2 = W-min P;
set q1 = E-max P;
set Q = Lower_Arc P;
now :: thesis: ( ( p1 <> p2 & LE p2,p1,P ) or ( p1 = p2 & LE p2,p1,P ) )
per cases ( p1 <> p2 or p1 = p2 ) ;
case A13: p1 <> p2 ; :: thesis: LE p2,p1,P
now :: thesis: ( ( 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 & LE p2,p1,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 & LE p2,p1,P ) )
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 ;
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: LE p2,p1,P
now :: thesis: ( ( p2 = W-min P & LE p2,p1,P ) or ( p2 <> W-min P & contradiction ) )
per cases ( p2 = W-min P or p2 <> W-min P ) ;
case p2 = W-min P ; :: thesis: LE p2,p1,P
hence LE p2,p1,P by ; :: thesis: verum
end;
end;
end;
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 ; :: 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 ; :: thesis: verum
end;
end;
end;
hence LE p2,p1,P ; :: thesis: verum
end;
end;