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