set p = |[(- 1),0]|;
A1: |[(- 1),0]| `1 = - 1 by EUCLID:52;
A2: |[(- 1),0]| `2 = 0 by EUCLID:52;
A3: |[(- 1),0]| <> 0. (TOP-REAL 2) by A1, EUCLID:52, EUCLID:54;
|[(- 1),0]| `2 <= - (|[(- 1),0]| `1) by A1, EUCLID:52;
then Sq_Circ . |[(- 1),0]| = |[((|[(- 1),0]| `1) / (sqrt (1 + (((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) ^2)))),((|[(- 1),0]| `2) / (sqrt (1 + (((|[(- 1),0]| `2) / (|[(- 1),0]| `1)) ^2))))]| by A1, A2, A3, JGRAPH_3:def 1;
hence Sq_Circ . |[(- 1),0]| = |[(- 1),0]| by A2, EUCLID:52, SQUARE_1:18; :: thesis: verum