let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 Sq_Circ or not x2 in proj1 Sq_Circ or not Sq_Circ . x1 = Sq_Circ . x2 or x1 = x2 )
assume A1: ( x1 in dom Sq_Circ & x2 in dom Sq_Circ & Sq_Circ . x1 = Sq_Circ . x2 ) ; :: thesis: x1 = x2
then reconsider p1 = x1 as Point of (TOP-REAL 2) ;
reconsider p2 = x2 as Point of (TOP-REAL 2) by A1;
set q = p1;
set p = p2;

per cases ( p1 = 0. (TOP-REAL 2) or ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) or ( p1 <> 0. (TOP-REAL 2) & not ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) & not ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) ;

suppose A2: p1 = 0. (TOP-REAL 2) ; :: thesis: x1 = x2

then A3: Sq_Circ . p1 = 0. (TOP-REAL 2) by Def1;

now

per cases ( p2 = 0. (TOP-REAL 2) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ;

case p2 = 0. (TOP-REAL 2) ; :: thesis: x1 = x2

hence x1 = x2 by A2; :: thesis: verum

end;

case A4: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ; :: thesis: contradiction

then Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by Def1;
then A5: ( (p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 & (p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 ) by A1, A3, EUCLID:56, JGRAPH_2:11;
((p2 `2 ) / (p2 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A6: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
then A7: p2 `1 = 0 * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A5, XCMPLX_1:88
.= 0 ;
p2 `2 = 0 * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A5, A6, XCMPLX_1:88
.= 0 ;
hence contradiction by A4, A7, EUCLID:57, EUCLID:58; :: thesis: verum

end;

case A8: ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ; :: thesis: contradiction

then Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by Def1;
then A9: ( (p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = 0 & (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = 0 ) by A1, A3, EUCLID:56, JGRAPH_2:11;
((p2 `1 ) / (p2 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p2 `1 ) / (p2 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A10: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
p2 `2 = 0 * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A9, A10, XCMPLX_1:88
.= 0 ;
hence contradiction by A8; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

suppose A12: ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ) ; :: thesis: x1 = x2

then A13: Sq_Circ . p1 = |[((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by Def1;
A14: ( |[((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| `1 = (p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & |[((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| `2 = (p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by EUCLID:56;
A15: 1 + (((p1 `2 ) / (p1 `1 )) ^2 ) > 0 by Lm1;
A16: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;

now

per cases ( p2 = 0. (TOP-REAL 2) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ;

case p2 = 0. (TOP-REAL 2) ; :: thesis: contradiction

then Sq_Circ . p2 = 0. (TOP-REAL 2) by Def1;
then A17: ( (p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) = 0 & (p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) = 0 ) by A1, A13, EUCLID:56, JGRAPH_2:11;
((p1 `2 ) / (p1 `1 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p1 `2 ) / (p1 `1 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A18: sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
then A19: p1 `1 = 0 * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A17, XCMPLX_1:88
.= 0 ;
p1 `2 = 0 * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A17, A18, XCMPLX_1:88
.= 0 ;
hence contradiction by A12, A19, EUCLID:57, EUCLID:58; :: thesis: verum

end;

case A20: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ; :: thesis: x1 = x2

then A21: Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by Def1;
then A22: ( (p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = (p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & (p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = (p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by A1, A13, A14, EUCLID:56;
A23: 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) > 0 by Lm1;
A24: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) ^2 by A22, XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by A23, SQUARE_1:def 4;
then A25: ((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A15, SQUARE_1:def 4;
((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) ^2 by A22, XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by A23, SQUARE_1:def 4;
then A26: ((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A15, SQUARE_1:def 4;

now

assume A27: p2 `1 = 0 ; :: thesis: contradiction
then p2 `2 = 0 by A20;
hence contradiction by A20, A27, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A28: (p2 `1 ) ^2 > 0 by SQUARE_1:74;
(((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) / ((p2 `1 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A25, XCMPLX_1:48;
then (((p2 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A28, XCMPLX_1:60;
then A29: (1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) * (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ) by A15, XCMPLX_1:88;

now

assume A30: p1 `1 = 0 ; :: thesis: contradiction
then p1 `2 = 0 by A12;
hence contradiction by A12, A30, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A31: (p1 `1 ) ^2 > 0 by SQUARE_1:74;

now

per cases ( p2 `2 = 0 or p2 `2 <> 0 ) ;

case A32: p2 `2 = 0 ; :: thesis: x1 = x2

then (p1 `2 ) ^2 = 0 by A15, A26, XCMPLX_1:50;
then A33: p1 `2 = 0 by XCMPLX_1:6;
then p2 = |[(p1 `1 ),0 ]| by A1, A13, A21, A32, EUCLID:57, SQUARE_1:83;
hence x1 = x2 by A33, EUCLID:57; :: thesis: verum

end;

case p2 `2 <> 0 ; :: thesis: x1 = x2

then A34: (p2 `2 ) ^2 > 0 by SQUARE_1:74;
(((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) / ((p2 `2 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A26, XCMPLX_1:48;
then (((p2 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A34, XCMPLX_1:60;
then (1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) * (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ) by A15, XCMPLX_1:88;
then (((p1 `1 ) ^2 ) / ((p1 `1 ) ^2 )) / ((p2 `1 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / ((p1 `1 ) ^2 ) by A29, XCMPLX_1:48;
then 1 / ((p2 `1 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / ((p1 `1 ) ^2 ) by A31, XCMPLX_1:60;
then (1 / ((p2 `1 ) ^2 )) * ((p2 `2 ) ^2 ) = (((p2 `2 ) ^2 ) * (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ))) / ((p1 `1 ) ^2 ) by XCMPLX_1:75;
then (1 / ((p2 `1 ) ^2 )) * ((p2 `2 ) ^2 ) = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by A34, XCMPLX_1:88;
then ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by XCMPLX_1:100;
then ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by XCMPLX_1:77;
then A35: 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) = 1 + (((p1 `2 ) / (p1 `1 )) ^2 ) by XCMPLX_1:77;
then p2 `1 = ((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A22, A24, XCMPLX_1:88;
then A36: p2 `1 = p1 `1 by A16, XCMPLX_1:88;
p2 `2 = ((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A22, A24, A35, XCMPLX_1:88;
then p2 `2 = p1 `2 by A16, XCMPLX_1:88;
then p2 = |[(p1 `1 ),(p1 `2 )]| by A36, EUCLID:57;
hence x1 = x2 by EUCLID:57; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

case A37: ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ; :: thesis: x1 = x2

then A38: ( ( p2 <> 0. (TOP-REAL 2) & p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2 ) ) ) by JGRAPH_2:23;
( |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 = (p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) & |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 = (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) by EUCLID:56;
then A39: ( (p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = (p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) & (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = (p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ) by A1, A13, A14, A37, Def1;
A40: 1 + (((p2 `1 ) / (p2 `2 )) ^2 ) > 0 by Lm1;
A41: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) ^2 by A39, XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by A40, SQUARE_1:def 4;
then A42: ((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A15, SQUARE_1:def 4;
((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) ^2 by A39, XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) ^2 ) by A40, SQUARE_1:def 4;
then A43: ((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A15, SQUARE_1:def 4;
p2 `2 <> 0 by A37;
then A44: (p2 `2 ) ^2 > 0 by SQUARE_1:74;
(((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) / ((p2 `2 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A43, XCMPLX_1:48;
then (((p2 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A44, XCMPLX_1:60;
then A45: (1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) * (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ) by A15, XCMPLX_1:88;

A46: now

assume A47: p1 `1 = 0 ; :: thesis: contradiction
then p1 `2 = 0 by A12;
hence contradiction by A12, A47, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A48: (p1 `1 ) ^2 > 0 by SQUARE_1:74;

now

per cases ( p2 `1 = 0 or p2 `1 <> 0 ) ;

case p2 `1 = 0 ; :: thesis: contradiction

then (p1 `1 ) ^2 = 0 by A15, A42, XCMPLX_1:50;
then A49: p1 `1 = 0 by XCMPLX_1:6;
then p1 `2 = 0 by A12;
hence contradiction by A12, A49, EUCLID:57, EUCLID:58; :: thesis: verum

end;

case A50: p2 `1 <> 0 ; :: thesis: x1 = x2

then A51: (p2 `1 ) ^2 > 0 by SQUARE_1:74;
(((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) / ((p2 `1 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A42, XCMPLX_1:48;
then (((p2 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) by A51, XCMPLX_1:60;
then (1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) * (1 + (((p1 `2 ) / (p1 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ) by A15, XCMPLX_1:88;
then (((p1 `1 ) ^2 ) / ((p1 `1 ) ^2 )) / ((p2 `1 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / ((p1 `1 ) ^2 ) by A45, XCMPLX_1:48;
then 1 / ((p2 `1 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / ((p1 `1 ) ^2 ) by A48, XCMPLX_1:60;
then (1 / ((p2 `1 ) ^2 )) * ((p2 `2 ) ^2 ) = (((p2 `2 ) ^2 ) * (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ))) / ((p1 `1 ) ^2 ) by XCMPLX_1:75;
then (1 / ((p2 `1 ) ^2 )) * ((p2 `2 ) ^2 ) = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by A44, XCMPLX_1:88;
then ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by XCMPLX_1:100;
then ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `2 ) ^2 ) / ((p1 `1 ) ^2 ) by XCMPLX_1:77;
then A52: ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2 by XCMPLX_1:77;
set a = (p1 `2 ) / (p1 `1 );
A53: ( ((p2 `2 ) / (p2 `1 )) * (p2 `1 ) = ((p1 `2 ) / (p1 `1 )) * (p2 `1 ) or ((p2 `2 ) / (p2 `1 )) * (p2 `1 ) = (- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ) ) by A52, SQUARE_1:109;

A54: now

per cases ( p2 `2 = ((p1 `2 ) / (p1 `1 )) * (p2 `1 ) or p2 `2 = (- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ) ) by A50, A53, XCMPLX_1:88;

case A55: p2 `2 = ((p1 `2 ) / (p1 `1 )) * (p2 `1 ) ; :: thesis: ( 1 <= (p1 `2 ) / (p1 `1 ) or - 1 >= (p1 `2 ) / (p1 `1 ) )

now

per cases ( p2 `1 > 0 or p2 `1 < 0 ) by A50;

case p2 `1 > 0 ; :: thesis: ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) )

then ( ( (p2 `1 ) / (p2 `1 ) <= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) <= (p2 `1 ) / (p2 `1 ) ) or ( (p2 `1 ) / (p2 `1 ) >= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (p2 `1 ) / (p2 `1 ) <= (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) ) ) by A38, A55, XREAL_1:74;
then A56: ( ( 1 <= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) <= 1 ) or ( 1 >= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & 1 <= (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) ) ) by A50, XCMPLX_1:60;
(((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) = (p1 `2 ) / (p1 `1 ) by A50, XCMPLX_1:90;
hence ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) ) by A56, XCMPLX_1:188; :: thesis: verum

end;

case p2 `1 < 0 ; :: thesis: ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) )

then ( ( (p2 `1 ) / (p2 `1 ) >= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) >= (p2 `1 ) / (p2 `1 ) ) or ( (p2 `1 ) / (p2 `1 ) <= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (p2 `1 ) / (p2 `1 ) >= (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) ) ) by A38, A55, XREAL_1:75;
then A57: ( ( 1 >= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) >= 1 ) or ( 1 <= (((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) & 1 >= (- (((p1 `2 ) / (p1 `1 )) * (p2 `1 ))) / (p2 `1 ) ) ) by A50, XCMPLX_1:60;
(((p1 `2 ) / (p1 `1 )) * (p2 `1 )) / (p2 `1 ) = (p1 `2 ) / (p1 `1 ) by A50, XCMPLX_1:90;
hence ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) ) by A57, XCMPLX_1:188; :: thesis: verum

end;

end;

end;

then ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & - 1 >= - (- ((p1 `2 ) / (p1 `1 ))) ) ) by XREAL_1:26;
hence ( 1 <= (p1 `2 ) / (p1 `1 ) or - 1 >= (p1 `2 ) / (p1 `1 ) ) ; :: thesis: verum

end;

case A58: p2 `2 = (- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ) ; :: thesis: ( 1 <= (p1 `2 ) / (p1 `1 ) or - 1 >= (p1 `2 ) / (p1 `1 ) )

now

per cases ( p2 `1 > 0 or p2 `1 < 0 ) by A50;

case p2 `1 > 0 ; :: thesis: ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) )

then ( ( (p2 `1 ) / (p2 `1 ) <= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) <= (p2 `1 ) / (p2 `1 ) ) or ( (p2 `1 ) / (p2 `1 ) >= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (p2 `1 ) / (p2 `1 ) <= (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) ) ) by A38, A58, XREAL_1:74;
then A59: ( ( 1 <= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) <= 1 ) or ( 1 >= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & 1 <= (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) ) ) by A50, XCMPLX_1:60;
A60: ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) = - ((p1 `2 ) / (p1 `1 )) by A50, XCMPLX_1:90;
( ( 1 <= - ((p1 `2 ) / (p1 `1 )) & - (((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 )) <= 1 ) or ( 1 >= - ((p1 `2 ) / (p1 `1 )) & 1 <= - (((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 )) ) ) by A50, A59, XCMPLX_1:90, XCMPLX_1:188;
hence ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) ) by A60; :: thesis: verum

end;

case p2 `1 < 0 ; :: thesis: ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) )

then ( ( (p2 `1 ) / (p2 `1 ) >= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) >= (p2 `1 ) / (p2 `1 ) ) or ( (p2 `1 ) / (p2 `1 ) <= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (p2 `1 ) / (p2 `1 ) >= (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) ) ) by A38, A58, XREAL_1:75;
then A61: ( ( 1 >= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) >= 1 ) or ( 1 <= ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) & 1 >= (- ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 ))) / (p2 `1 ) ) ) by A50, XCMPLX_1:60;
A62: ((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 ) = - ((p1 `2 ) / (p1 `1 )) by A50, XCMPLX_1:90;
( ( 1 >= - ((p1 `2 ) / (p1 `1 )) & - (((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 )) >= 1 ) or ( 1 <= - ((p1 `2 ) / (p1 `1 )) & 1 >= - (((- ((p1 `2 ) / (p1 `1 ))) * (p2 `1 )) / (p2 `1 )) ) ) by A50, A61, XCMPLX_1:90, XCMPLX_1:188;
hence ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & 1 <= - ((p1 `2 ) / (p1 `1 )) ) ) by A62; :: thesis: verum

end;

end;

end;

then ( ( 1 <= (p1 `2 ) / (p1 `1 ) & - ((p1 `2 ) / (p1 `1 )) <= 1 ) or ( 1 >= (p1 `2 ) / (p1 `1 ) & - 1 >= - (- ((p1 `2 ) / (p1 `1 ))) ) ) by XREAL_1:26;
hence ( 1 <= (p1 `2 ) / (p1 `1 ) or - 1 >= (p1 `2 ) / (p1 `1 ) ) ; :: thesis: verum

end;

end;

end;

A63: ( ( (p1 `1 ) * ((p1 `2 ) / (p1 `1 )) <= p1 `1 & - (p1 `1 ) <= (p1 `1 ) * ((p1 `2 ) / (p1 `1 )) ) or ( (p1 `1 ) * ((p1 `2 ) / (p1 `1 )) >= p1 `1 & (p1 `1 ) * ((p1 `2 ) / (p1 `1 )) <= - (p1 `1 ) ) ) by A12, A46, XCMPLX_1:88;

A64: now

per cases ( p1 `1 > 0 or p1 `1 < 0 ) by A46;

case A65: p1 `1 > 0 ; :: thesis: ( ( (p1 `2 ) / (p1 `1 ) <= 1 & - 1 <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= 1 & (p1 `2 ) / (p1 `1 ) <= - 1 ) )

then ( ( (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) <= (p1 `1 ) / (p1 `1 ) & (- (p1 `1 )) / (p1 `1 ) <= (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) ) or ( (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) >= (p1 `1 ) / (p1 `1 ) & (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) <= (- (p1 `1 )) / (p1 `1 ) ) ) by A63, XREAL_1:74;
then A66: ( ( (p1 `2 ) / (p1 `1 ) <= (p1 `1 ) / (p1 `1 ) & (- (p1 `1 )) / (p1 `1 ) <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= (p1 `1 ) / (p1 `1 ) & (p1 `2 ) / (p1 `1 ) <= (- (p1 `1 )) / (p1 `1 ) ) ) by A65, XCMPLX_1:90;
(p1 `1 ) / (p1 `1 ) = 1 by A65, XCMPLX_1:60;
hence ( ( (p1 `2 ) / (p1 `1 ) <= 1 & - 1 <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= 1 & (p1 `2 ) / (p1 `1 ) <= - 1 ) ) by A66, XCMPLX_1:188; :: thesis: verum

end;

case A67: p1 `1 < 0 ; :: thesis: ( ( (p1 `2 ) / (p1 `1 ) <= 1 & - 1 <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= 1 & (p1 `2 ) / (p1 `1 ) <= - 1 ) )

then A68: ( ( (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) >= (p1 `1 ) / (p1 `1 ) & (- (p1 `1 )) / (p1 `1 ) >= (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) ) or ( (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) <= (p1 `1 ) / (p1 `1 ) & (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) / (p1 `1 ) >= (- (p1 `1 )) / (p1 `1 ) ) ) by A63, XREAL_1:75;
A69: (p1 `1 ) / (p1 `1 ) = 1 by A67, XCMPLX_1:60;
(- (p1 `1 )) / (p1 `1 ) = - 1 by A67, XCMPLX_1:198;
hence ( ( (p1 `2 ) / (p1 `1 ) <= 1 & - 1 <= (p1 `2 ) / (p1 `1 ) ) or ( (p1 `2 ) / (p1 `1 ) >= 1 & (p1 `2 ) / (p1 `1 ) <= - 1 ) ) by A67, A68, A69, XCMPLX_1:90; :: thesis: verum

end;

end;

end;

A70: now

per cases ( (p1 `2 ) / (p1 `1 ) = 1 or (p1 `2 ) / (p1 `1 ) = - 1 ) by A54, A64, XXREAL_0:1;

case (p1 `2 ) / (p1 `1 ) = 1 ; :: thesis: ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2

then ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) = 1 by A52, XCMPLX_1:77;
then A71: (p2 `2 ) ^2 = (p2 `1 ) ^2 by XCMPLX_1:58;
((p2 `1 ) / (p2 `2 )) ^2 = ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) by XCMPLX_1:77;
hence ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2 by A52, A71, XCMPLX_1:77; :: thesis: verum

end;

case (p1 `2 ) / (p1 `1 ) = - 1 ; :: thesis: ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2

then ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) = 1 by A52, XCMPLX_1:77;
then A72: (p2 `2 ) ^2 = (p2 `1 ) ^2 by XCMPLX_1:58;
((p2 `1 ) / (p2 `2 )) ^2 = ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) by XCMPLX_1:77;
hence ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `2 ) / (p1 `1 )) ^2 by A52, A72, XCMPLX_1:77; :: thesis: verum

end;

end;

end;

then p2 `1 = ((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A39, A41, XCMPLX_1:88;
then A73: p2 `1 = p1 `1 by A16, XCMPLX_1:88;
p2 `2 = ((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))) * (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))) by A39, A41, A70, XCMPLX_1:88;
then p2 `2 = p1 `2 by A16, XCMPLX_1:88;
then p2 = |[(p1 `1 ),(p1 `2 )]| by A73, EUCLID:57;
hence x1 = x2 by EUCLID:57; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

suppose A74: ( p1 <> 0. (TOP-REAL 2) & not ( p1 `2 <= p1 `1 & - (p1 `1 ) <= p1 `2 ) & not ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1 ) ) ) ; :: thesis: x1 = x2

then A75: Sq_Circ . p1 = |[((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| by Def1;
A76: ( |[((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| `1 = (p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) & |[((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))))]| `2 = (p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) by EUCLID:56;
A77: 1 + (((p1 `1 ) / (p1 `2 )) ^2 ) > 0 by Lm1;
A78: sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
A79: ( ( p1 `1 <= p1 `2 & - (p1 `2 ) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2 ) ) ) by A74, JGRAPH_2:23;

now

per cases ( p2 = 0. (TOP-REAL 2) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ;

case p2 = 0. (TOP-REAL 2) ; :: thesis: contradiction

then Sq_Circ . p2 = 0. (TOP-REAL 2) by Def1;
then A80: ( (p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) = 0 & (p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) = 0 ) by A1, A75, EUCLID:56, JGRAPH_2:11;
((p1 `1 ) / (p1 `2 )) ^2 >= 0 by XREAL_1:65;
then 1 + (((p1 `1 ) / (p1 `2 )) ^2 ) >= 1 + 0 by XREAL_1:9;
then A81: sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) >= 1 by SQUARE_1:83, SQUARE_1:94;
p1 `2 = 0 * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A80, A81, XCMPLX_1:88
.= 0 ;
hence contradiction by A74; :: thesis: verum

end;

case A83: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ; :: thesis: x1 = x2

then Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by Def1;
then A84: ( (p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = (p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) & (p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = (p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) by A1, A75, A76, EUCLID:56;
A85: 1 + (((p2 `2 ) / (p2 `1 )) ^2 ) > 0 by Lm1;
A86: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) ^2 by A84, XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by A85, SQUARE_1:def 4;
then A87: ((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `1 ) ^2 ) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A77, SQUARE_1:def 4;
((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) ^2 by A84, XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ^2 ) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by A85, SQUARE_1:def 4;
then A88: ((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = ((p1 `2 ) ^2 ) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A77, SQUARE_1:def 4;

now

assume A89: p2 `1 = 0 ; :: thesis: contradiction
then p2 `2 = 0 by A83;
hence contradiction by A83, A89, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A90: (p2 `1 ) ^2 > 0 by SQUARE_1:74;
(((p2 `1 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) / ((p2 `1 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A87, XCMPLX_1:48;
then (((p2 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A90, XCMPLX_1:60;
then A91: (1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) * (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ) by A77, XCMPLX_1:88;
A92: p1 `2 <> 0 by A74;
then A93: (p1 `2 ) ^2 > 0 by SQUARE_1:74;

now

per cases ( p2 `2 = 0 or p2 `2 <> 0 ) ;

case p2 `2 = 0 ; :: thesis: contradiction

then (p1 `2 ) ^2 = 0 by A77, A88, XCMPLX_1:50;
then p1 `2 = 0 by XCMPLX_1:6;
hence contradiction by A74; :: thesis: verum

end;

case A94: p2 `2 <> 0 ; :: thesis: x1 = x2

then A95: (p2 `2 ) ^2 > 0 by SQUARE_1:74;
(((p2 `2 ) ^2 ) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) / ((p2 `2 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A88, XCMPLX_1:48;
then (((p2 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A95, XCMPLX_1:60;
then (1 / (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) * (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ) by A77, XCMPLX_1:88;
then (((p1 `2 ) ^2 ) / ((p1 `2 ) ^2 )) / ((p2 `2 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / ((p1 `2 ) ^2 ) by A91, XCMPLX_1:48;
then 1 / ((p2 `2 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / ((p1 `2 ) ^2 ) by A93, XCMPLX_1:60;
then (1 / ((p2 `2 ) ^2 )) * ((p2 `1 ) ^2 ) = (((p2 `1 ) ^2 ) * (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ))) / ((p1 `2 ) ^2 ) by XCMPLX_1:75;
then (1 / ((p2 `2 ) ^2 )) * ((p2 `1 ) ^2 ) = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by A90, XCMPLX_1:88;
then ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by XCMPLX_1:100;
then ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by XCMPLX_1:77;
then A96: ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2 by XCMPLX_1:77;
then A97: ( (p2 `1 ) / (p2 `2 ) = (p1 `1 ) / (p1 `2 ) or (p2 `1 ) / (p2 `2 ) = - ((p1 `1 ) / (p1 `2 )) ) by SQUARE_1:109;
set a = (p1 `1 ) / (p1 `2 );

A98: now

per cases ( p2 `1 = ((p1 `1 ) / (p1 `2 )) * (p2 `2 ) or p2 `1 = (- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ) ) by A94, A97, XCMPLX_1:88;

case A99: p2 `1 = ((p1 `1 ) / (p1 `2 )) * (p2 `2 ) ; :: thesis: ( 1 <= (p1 `1 ) / (p1 `2 ) or - 1 >= (p1 `1 ) / (p1 `2 ) )

now

per cases ( p2 `2 > 0 or p2 `2 < 0 ) by A94;

case p2 `2 > 0 ; :: thesis: ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) )

then ( ( (p2 `2 ) / (p2 `2 ) <= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) <= (p2 `2 ) / (p2 `2 ) ) or ( (p2 `2 ) / (p2 `2 ) >= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (p2 `2 ) / (p2 `2 ) <= (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) ) ) by A83, A99, XREAL_1:74;
then A100: ( ( 1 <= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) <= 1 ) or ( 1 >= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & 1 <= (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) ) ) by A94, XCMPLX_1:60;
(((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) = (p1 `1 ) / (p1 `2 ) by A94, XCMPLX_1:90;
hence ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) ) by A100, XCMPLX_1:188; :: thesis: verum

end;

case p2 `2 < 0 ; :: thesis: ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) )

then ( ( (p2 `2 ) / (p2 `2 ) >= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) >= (p2 `2 ) / (p2 `2 ) ) or ( (p2 `2 ) / (p2 `2 ) <= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (p2 `2 ) / (p2 `2 ) >= (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) ) ) by A83, A99, XREAL_1:75;
then A101: ( ( 1 >= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) >= 1 ) or ( 1 <= (((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) & 1 >= (- (((p1 `1 ) / (p1 `2 )) * (p2 `2 ))) / (p2 `2 ) ) ) by A94, XCMPLX_1:60;
(((p1 `1 ) / (p1 `2 )) * (p2 `2 )) / (p2 `2 ) = (p1 `1 ) / (p1 `2 ) by A94, XCMPLX_1:90;
hence ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) ) by A101, XCMPLX_1:188; :: thesis: verum

end;

end;

end;

then ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & - 1 >= - (- ((p1 `1 ) / (p1 `2 ))) ) ) by XREAL_1:26;
hence ( 1 <= (p1 `1 ) / (p1 `2 ) or - 1 >= (p1 `1 ) / (p1 `2 ) ) ; :: thesis: verum

end;

case A102: p2 `1 = (- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ) ; :: thesis: ( 1 <= (p1 `1 ) / (p1 `2 ) or - 1 >= (p1 `1 ) / (p1 `2 ) )

now

per cases ( p2 `2 > 0 or p2 `2 < 0 ) by A94;

case p2 `2 > 0 ; :: thesis: ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) )

then ( ( (p2 `2 ) / (p2 `2 ) <= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) <= (p2 `2 ) / (p2 `2 ) ) or ( (p2 `2 ) / (p2 `2 ) >= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (p2 `2 ) / (p2 `2 ) <= (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) ) ) by A83, A102, XREAL_1:74;
then A103: ( ( 1 <= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) <= 1 ) or ( 1 >= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & 1 <= (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) ) ) by A94, XCMPLX_1:60;
A104: ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) = - ((p1 `1 ) / (p1 `2 )) by A94, XCMPLX_1:90;
( ( 1 <= - ((p1 `1 ) / (p1 `2 )) & - (((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 )) <= 1 ) or ( 1 >= - ((p1 `1 ) / (p1 `2 )) & 1 <= - (((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 )) ) ) by A94, A103, XCMPLX_1:90, XCMPLX_1:188;
hence ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) ) by A104; :: thesis: verum

end;

case p2 `2 < 0 ; :: thesis: ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) )

then ( ( (p2 `2 ) / (p2 `2 ) >= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) >= (p2 `2 ) / (p2 `2 ) ) or ( (p2 `2 ) / (p2 `2 ) <= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (p2 `2 ) / (p2 `2 ) >= (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) ) ) by A83, A102, XREAL_1:75;
then A105: ( ( 1 >= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) >= 1 ) or ( 1 <= ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) & 1 >= (- ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 ))) / (p2 `2 ) ) ) by A94, XCMPLX_1:60;
A106: ((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 ) = - ((p1 `1 ) / (p1 `2 )) by A94, XCMPLX_1:90;
( ( 1 >= - ((p1 `1 ) / (p1 `2 )) & - (((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 )) >= 1 ) or ( 1 <= - ((p1 `1 ) / (p1 `2 )) & 1 >= - (((- ((p1 `1 ) / (p1 `2 ))) * (p2 `2 )) / (p2 `2 )) ) ) by A94, A105, XCMPLX_1:90, XCMPLX_1:188;
hence ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & 1 <= - ((p1 `1 ) / (p1 `2 )) ) ) by A106; :: thesis: verum

end;

end;

end;

then ( ( 1 <= (p1 `1 ) / (p1 `2 ) & - ((p1 `1 ) / (p1 `2 )) <= 1 ) or ( 1 >= (p1 `1 ) / (p1 `2 ) & - 1 >= - (- ((p1 `1 ) / (p1 `2 ))) ) ) by XREAL_1:26;
hence ( 1 <= (p1 `1 ) / (p1 `2 ) or - 1 >= (p1 `1 ) / (p1 `2 ) ) ; :: thesis: verum

end;

end;

end;

A107: ( ( (p1 `2 ) * ((p1 `1 ) / (p1 `2 )) <= p1 `2 & - (p1 `2 ) <= (p1 `2 ) * ((p1 `1 ) / (p1 `2 )) ) or ( (p1 `2 ) * ((p1 `1 ) / (p1 `2 )) >= p1 `2 & (p1 `2 ) * ((p1 `1 ) / (p1 `2 )) <= - (p1 `2 ) ) ) by A79, A92, XCMPLX_1:88;

A108: now

per cases ( p1 `2 > 0 or p1 `2 < 0 ) by A92;

case A109: p1 `2 > 0 ; :: thesis: ( ( (p1 `1 ) / (p1 `2 ) <= 1 & - 1 <= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) >= 1 & (p1 `1 ) / (p1 `2 ) <= - 1 ) )

then A110: ( ( (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) <= (p1 `2 ) / (p1 `2 ) & (- (p1 `2 )) / (p1 `2 ) <= (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) ) or ( (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) >= (p1 `2 ) / (p1 `2 ) & (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) <= (- (p1 `2 )) / (p1 `2 ) ) ) by A107, XREAL_1:74;
A111: (p1 `2 ) / (p1 `2 ) = 1 by A109, XCMPLX_1:60;
(- (p1 `2 )) / (p1 `2 ) = - 1 by A109, XCMPLX_1:198;
hence ( ( (p1 `1 ) / (p1 `2 ) <= 1 & - 1 <= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) >= 1 & (p1 `1 ) / (p1 `2 ) <= - 1 ) ) by A109, A110, A111, XCMPLX_1:90; :: thesis: verum

end;

case A112: p1 `2 < 0 ; :: thesis: ( ( (p1 `1 ) / (p1 `2 ) <= 1 & - 1 <= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) >= 1 & (p1 `1 ) / (p1 `2 ) <= - 1 ) )

then ( ( (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) >= (p1 `2 ) / (p1 `2 ) & (- (p1 `2 )) / (p1 `2 ) >= (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) ) or ( (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) <= (p1 `2 ) / (p1 `2 ) & (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) / (p1 `2 ) >= (- (p1 `2 )) / (p1 `2 ) ) ) by A107, XREAL_1:75;
then ( ( (p1 `1 ) / (p1 `2 ) >= (p1 `2 ) / (p1 `2 ) & (- (p1 `2 )) / (p1 `2 ) >= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) <= (p1 `2 ) / (p1 `2 ) & (p1 `1 ) / (p1 `2 ) >= (- (p1 `2 )) / (p1 `2 ) ) ) by A112, XCMPLX_1:90;
hence ( ( (p1 `1 ) / (p1 `2 ) <= 1 & - 1 <= (p1 `1 ) / (p1 `2 ) ) or ( (p1 `1 ) / (p1 `2 ) >= 1 & (p1 `1 ) / (p1 `2 ) <= - 1 ) ) by A112, XCMPLX_1:60, XCMPLX_1:198; :: thesis: verum

end;

end;

end;

A113: now

per cases ( (p1 `1 ) / (p1 `2 ) = 1 or (p1 `1 ) / (p1 `2 ) = - 1 ) by A98, A108, XXREAL_0:1;

case (p1 `1 ) / (p1 `2 ) = 1 ; :: thesis: ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2

then ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) = 1 by A96, XCMPLX_1:77;
then A114: (p2 `1 ) ^2 = (p2 `2 ) ^2 by XCMPLX_1:58;
((p2 `2 ) / (p2 `1 )) ^2 = ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) by XCMPLX_1:77;
hence ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2 by A96, A114, XCMPLX_1:77; :: thesis: verum

end;

case (p1 `1 ) / (p1 `2 ) = - 1 ; :: thesis: ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2

then ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) = 1 by A96, XCMPLX_1:77;
then A115: (p2 `1 ) ^2 = (p2 `2 ) ^2 by XCMPLX_1:58;
((p2 `2 ) / (p2 `1 )) ^2 = ((p2 `2 ) ^2 ) / ((p2 `1 ) ^2 ) by XCMPLX_1:77;
hence ((p2 `2 ) / (p2 `1 )) ^2 = ((p1 `1 ) / (p1 `2 )) ^2 by A96, A115, XCMPLX_1:77; :: thesis: verum

end;

end;

end;

then p2 `2 = ((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A84, A86, XCMPLX_1:88;
then A116: p2 `2 = p1 `2 by A78, XCMPLX_1:88;
p2 `1 = ((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A84, A86, A113, XCMPLX_1:88;
then p2 `1 = p1 `1 by A78, XCMPLX_1:88;
then p2 = |[(p1 `1 ),(p1 `2 )]| by A116, EUCLID:57;
hence x1 = x2 by EUCLID:57; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

case A117: ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ; :: thesis: x1 = x2

A119: Sq_Circ . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A117, Def1;
then A120: ( (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = (p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) & (p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = (p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ) by A1, A75, A76, EUCLID:56;
A121: 1 + (((p2 `1 ) / (p2 `2 )) ^2 ) > 0 by Lm1;
A122: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by Lm1, SQUARE_1:93;
((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) ^2 by A120, XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by A121, SQUARE_1:def 4;
then A123: ((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A77, SQUARE_1:def 4;
((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) ^2 by A120, XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / ((sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ^2 ) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by XCMPLX_1:77;
then ((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / ((sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) ^2 ) by A121, SQUARE_1:def 4;
then A124: ((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A77, SQUARE_1:def 4;
p2 `2 <> 0 by A117;
then A125: (p2 `2 ) ^2 > 0 by SQUARE_1:74;
(((p2 `2 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) / ((p2 `2 ) ^2 ) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A123, XCMPLX_1:48;
then (((p2 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A125, XCMPLX_1:60;
then A126: (1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) * (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) = ((p1 `2 ) ^2 ) / ((p2 `2 ) ^2 ) by A77, XCMPLX_1:88;
p1 `2 <> 0 by A74;
then A127: (p1 `2 ) ^2 > 0 by SQUARE_1:74;

now

per cases ( p2 `1 = 0 or p2 `1 <> 0 ) ;

case A128: p2 `1 = 0 ; :: thesis: x1 = x2

then (p1 `1 ) ^2 = 0 by A77, A124, XCMPLX_1:50;
then A129: p1 `1 = 0 by XCMPLX_1:6;
then p2 = |[0 ,(p1 `2 )]| by A1, A75, A119, A128, EUCLID:57, SQUARE_1:83;
hence x1 = x2 by A129, EUCLID:57; :: thesis: verum

end;

case p2 `1 <> 0 ; :: thesis: x1 = x2

then A130: (p2 `1 ) ^2 > 0 by SQUARE_1:74;
(((p2 `1 ) ^2 ) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) / ((p2 `1 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A124, XCMPLX_1:48;
then (((p2 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by XCMPLX_1:48;
then 1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) by A130, XCMPLX_1:60;
then (1 / (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) * (1 + (((p1 `1 ) / (p1 `2 )) ^2 )) = ((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ) by A77, XCMPLX_1:88;
then (((p1 `2 ) ^2 ) / ((p1 `2 ) ^2 )) / ((p2 `2 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / ((p1 `2 ) ^2 ) by A126, XCMPLX_1:48;
then 1 / ((p2 `2 ) ^2 ) = (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 )) / ((p1 `2 ) ^2 ) by A127, XCMPLX_1:60;
then (1 / ((p2 `2 ) ^2 )) * ((p2 `1 ) ^2 ) = (((p2 `1 ) ^2 ) * (((p1 `1 ) ^2 ) / ((p2 `1 ) ^2 ))) / ((p1 `2 ) ^2 ) by XCMPLX_1:75;
then (1 / ((p2 `2 ) ^2 )) * ((p2 `1 ) ^2 ) = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by A130, XCMPLX_1:88;
then ((p2 `1 ) ^2 ) / ((p2 `2 ) ^2 ) = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by XCMPLX_1:100;
then ((p2 `1 ) / (p2 `2 )) ^2 = ((p1 `1 ) ^2 ) / ((p1 `2 ) ^2 ) by XCMPLX_1:77;
then A131: 1 + (((p2 `1 ) / (p2 `2 )) ^2 ) = 1 + (((p1 `1 ) / (p1 `2 )) ^2 ) by XCMPLX_1:77;
then p2 `2 = ((p1 `2 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A120, A122, XCMPLX_1:88;
then A132: p2 `2 = p1 `2 by A78, XCMPLX_1:88;
p2 `1 = ((p1 `1 ) / (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 )))) * (sqrt (1 + (((p1 `1 ) / (p1 `2 )) ^2 ))) by A120, A122, A131, XCMPLX_1:88;
then p2 `1 = p1 `1 by A78, XCMPLX_1:88;
then p2 = |[(p1 `1 ),(p1 `2 )]| by A132, EUCLID:57;
hence x1 = x2 by EUCLID:57; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;