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 that
A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and
A2: ( p2 `2 >= 0 or p2 `1 >= 0 ) and
A3: LE p1,p2,P ; :: thesis: ( p1 `2 >= 0 or p1 `1 >= 0 )
A4: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th34;
A5: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then A6: p2 in P by A3, JORDAN7:5;
A7: Lower_Arc P is_an_arc_of E-max P, W-min P by A5, JORDAN6:def 9;

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

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

then p2 in Upper_Arc P by A6, A4;
then p1 in Upper_Arc P by A1, A3, Th44;
then ex p8 being Point of (TOP-REAL 2) st
( p8 = p1 & p8 in P & p8 `2 >= 0 ) by A4;
hence ( p1 `2 >= 0 or p1 `1 >= 0 ) ; :: thesis: verum

end;

suppose A8: ( 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 A9: not p2 in Upper_Arc P by A4;

now :: thesis: ( ( p1 in Upper_Arc P & p2 in Lower_Arc P & not p2 = W-min P & ( p1 `2 >= 0 or p1 `1 >= 0 ) ) 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 & ( p1 `2 >= 0 or p1 `1 >= 0 ) ) )

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 A3, A9;

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 ex p8 being Point of (TOP-REAL 2) st
( p8 = p1 & p8 in P & p8 `2 >= 0 ) by A4;
hence ( p1 `2 >= 0 or p1 `1 >= 0 ) ; :: 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 )

now :: thesis: not p1 = W-min P

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

end;

hence ( p1 `2 >= 0 or p1 `1 >= 0 ) by A1, A3, A8, Th48; :: thesis: verum

end;

end;

end;

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

end;

end;