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; verum