theorem :: JGRAPH_6:11

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds
Sq_Circ . |[(- 1),0]| = W-min P by Th10, JGRAPH_5:29;