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 A1: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p2 in Upper_Arc P & LE p1,p2,P ) ; :: thesis: p1 in Upper_Arc P
then A2: P is being_simple_closed_curve by JGRAPH_3:36;
then A3: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;
set P4b = Lower_Arc P;
A4: ( Lower_Arc P is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) by A2, JORDAN6:def 9;
then E-max P in (Upper_Arc P) /\ (Lower_Arc P) by TARSKI:def 2;
then A5: E-max P in Upper_Arc P by XBOOLE_0:def 4;
A6: ( ( 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 A1, JORDAN6:def 10;

now

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

end;

hence p1 in Upper_Arc P ; :: thesis: verum