set p = |[(- 1),0 ]|;
A1: |[(- 1),0 ]| `1 = - 1 by EUCLID:56;
A2: |[(- 1),0 ]| `2 = 0 by EUCLID:56;
A3: |[(- 1),0 ]| <> 0. (TOP-REAL 2) by A1, EUCLID:56, EUCLID:58;
|[(- 1),0 ]| `2 <= - (|[(- 1),0 ]| `1 ) by A1, EUCLID:56;
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:56, SQUARE_1:83; :: thesis: verum