theorem Th34: :: JGRAPH_5:34

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }