theorem Th30: :: JGRAPH_5:30
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
E-max P = |[1,0]|