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 `2 >= 0 or p2 `1 >= 0 ) & LE p1,p2,P & not p1 `2 >= 0 holds
p1 `1 >= 0
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 `2 >= 0 or p2 `1 >= 0 ) & LE p1,p2,P & not p1 `2 >= 0 implies p1 `1 >= 0 )
assume A1: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & ( p2 `2 >= 0 or p2 `1 >= 0 ) & LE p1,p2,P ) ; :: thesis: ( p1 `2 >= 0 or p1 `1 >= 0 )
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;
A4: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & ( p2 `2 >= 0 or p2 `1 >= 0 ) & LE p1,p2,P ) by A1, A2, JORDAN7:5;
A5: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th37;

per cases ( p2 `2 >= 0 or ( p2 `2 < 0 & p2 `1 >= 0 ) ) by A1;

suppose p2 `2 >= 0 ; :: thesis: ( p1 `2 >= 0 or p1 `1 >= 0 )

then p2 in Upper_Arc P by A4, A5;
then p1 in Upper_Arc P by A1, Th47;
then consider p8 being Point of (TOP-REAL 2) such that
A6: ( p8 = p1 & p8 in P & p8 `2 >= 0 ) by A5;
thus ( p1 `2 >= 0 or p1 `1 >= 0 ) by A6; :: thesis: verum

end;

suppose A7: ( p2 `2 < 0 & p2 `1 >= 0 ) ; :: thesis: ( p1 `2 >= 0 or p1 `1 >= 0 )

then for p8 being Point of (TOP-REAL 2) holds
( not p8 = p2 or not p8 in P or not p8 `2 >= 0 ) ;
then A8: not p2 in Upper_Arc P by A5;

now

per cases ( ( p1 in Upper_Arc P & p2 in Lower_Arc P & not p2 = W-min 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, A8, JORDAN6:def 10;

case ( p1 in Upper_Arc P & p2 in Lower_Arc P & not p2 = W-min P ) ; :: thesis: ( p1 `2 >= 0 or p1 `1 >= 0 )

then consider p8 being Point of (TOP-REAL 2) such that
A9: ( p8 = p1 & p8 in P & p8 `2 >= 0 ) by A5;
thus ( p1 `2 >= 0 or p1 `1 >= 0 ) by A9; :: thesis: verum

end;

case A10: ( 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 ) ; :: thesis: ( p1 `2 >= 0 or p1 `1 >= 0 )

consider p8 being Point of (TOP-REAL 2);

now

assume A11: p1 = W-min P ; :: thesis: contradiction
then LE p2,p1, Lower_Arc P, E-max P, W-min P by A3, A10, JORDAN5C:10;
hence contradiction by A3, A10, A11, JORDAN5C:12; :: thesis: verum

end;

hence ( p1 `2 >= 0 or p1 `1 >= 0 ) by A1, A7, Th51; :: thesis: verum

end;

end;

end;

hence ( p1 `2 >= 0 or p1 `1 >= 0 ) ; :: thesis: verum

end;

end;