let p1, p2 be Point of (TOP-REAL 2); 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); ( 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
; ( 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;