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 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 = (Upper_Arc P) \/ (Lower_Arc P) by A1, JORDAN6:def 9;

A6: not p1 = W-min P by A1, A3, A4, JORDAN7:3;

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 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 = (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
( ( 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 A2, A3, A5, XBOOLE_0:def 3;

end;

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 A1, JORDAN6:def 8;

set q1 = W-min P;

set q2 = E-max P;

set Q = Upper_Arc P;

end;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 ) )end;

hence
LE p2,p1,P
; :: thesis: verumper cases
( p1 <> p2 or p1 = p2 )
;

end;

case A9:
p1 <> p2
; :: thesis: LE p2,p1,P

end;

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 ) )end;

hence
LE p2,p1,P
; :: thesis: verumper 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 A7, A8, A9, JORDAN5C:14;

end;

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

end;

now :: thesis: ( ( p2 = W-min P & LE p2,p1,P ) or ( p2 <> W-min P & contradiction ) )

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

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 A1, JORDAN6:50;

set q2 = W-min P;

set q1 = E-max P;

set Q = Lower_Arc P;

end;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 ) )end;

hence
LE p2,p1,P
; :: thesis: verumper cases
( p1 <> p2 or p1 = p2 )
;

end;

case A13:
p1 <> p2
; :: thesis: LE p2,p1,P

end;

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 ) )end;

hence
LE p2,p1,P
; :: thesis: verumper 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 A11, A12, A13, JORDAN5C:14;

end;

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

end;

now :: thesis: ( ( p2 = W-min P & LE p2,p1,P ) or ( p2 <> W-min P & contradiction ) )

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