let p1, p2 be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p2 in Upper_Arc P & LE p1,p2,P holds
p1 in Upper_Arc P
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p2 in Upper_Arc P & LE p1,p2,P implies p1 in Upper_Arc P )
assume that
A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and
A2: p2 in Upper_Arc P and
A3: LE p1,p2,P ; :: thesis: p1 in Upper_Arc P
set P4b = Lower_Arc P;
A4: ( ( p1 in Upper_Arc P & p2 in Lower_Arc P & not p2 = W-min P ) or ( p1 in Upper_Arc P & p2 in Upper_Arc P & LE p1,p2, Upper_Arc P, W-min P, E-max P ) or ( p1 in Lower_Arc P & p2 in Lower_Arc P & not p2 = W-min P & LE p1,p2, Lower_Arc P, E-max P, W-min P ) ) by A3;
A5: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then A6: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;
A7: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A5, JORDAN6:def 9;
then E-max P in (Upper_Arc P) /\ (Lower_Arc P) by TARSKI:def 2;
then A8: E-max P in Upper_Arc P by XBOOLE_0:def 4;

now :: thesis: p1 in Upper_Arc P

assume A9: not p1 in Upper_Arc P ; :: thesis: contradiction
then p2 in (Upper_Arc P) /\ (Lower_Arc P) by A2, A4, XBOOLE_0:def 4;
then A10: p2 = E-max P by A7, A4, A9, TARSKI:def 2;
then LE p2,p1, Lower_Arc P, E-max P, W-min P by A6, A4, A9, JORDAN5C:10;
hence contradiction by A6, A8, A4, A9, A10, JORDAN5C:12; :: thesis: verum

end;

hence p1 in Upper_Arc P ; :: thesis: verum