theorem Th49: :: JGRAPH_5:49

for p1, p2 being 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