let Kb, Cb be Subset of (TOP-REAL 2); :: thesis: ( Kb = { p where p is Point of (TOP-REAL 2) : ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| <= 1 } implies Sq_Circ .: Kb = Cb )
assume A1: ( Kb = { p where p is Point of (TOP-REAL 2) : ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| <= 1 } ) ; :: thesis: Sq_Circ .: Kb = Cb
thus Sq_Circ .: Kb c= Cb :: according to XBOOLE_0:def 10 :: thesis: Cb c= Sq_Circ .: Kb

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Sq_Circ .: Kb or y in Cb )
assume y in Sq_Circ .: Kb ; :: thesis: y in Cb
then consider x being set such that
A2: ( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) by FUNCT_1:def 12;
consider q being Point of (TOP-REAL 2) such that
A3: ( q = x & - 1 <= q `1 & q `1 <= 1 & - 1 <= q `2 & q `2 <= 1 ) by A1, A2;

now

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

case A4: q = 0. (TOP-REAL 2) ; :: thesis: ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| <= 1 )

then A5: Sq_Circ . q = q by JGRAPH_3:def 1;
|.q.| = 0 by A4, TOPRNS_1:24;
hence ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| <= 1 ) by A2, A3, A5; :: thesis: verum

end;

case A6: ( q <> 0. (TOP-REAL 2) & ( ( q `2 <= q `1 & - (q `1 ) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ) ; :: thesis: ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| <= 1 )

then A7: Sq_Circ . q = |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]| by JGRAPH_3:def 1;
A8: ( |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]| `1 = (q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) & |[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]| `2 = (q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ) by EUCLID:56;
A9: 1 + (((q `2 ) / (q `1 )) ^2 ) > 0 by XREAL_1:36, XREAL_1:65;

A10: now

assume A11: q `1 = 0 ; :: thesis: contradiction
then q `2 = 0 by A6;
hence contradiction by A6, A11, EUCLID:57, EUCLID:58; :: thesis: verum

end;

then A12: (q `1 ) ^2 > 0 by SQUARE_1:74;
(q `1 ) ^2 <= 1 ^2 by A3, SQUARE_1:119;
then A13: sqrt ((q `1 ) ^2 ) <= 1 by A12, SQUARE_1:83, SQUARE_1:94;
|.|[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]|.| ^2 = (((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))) ^2 ) + (((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))) ^2 ) by A8, JGRAPH_3:10
.= (((q `1 ) ^2 ) / ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )) + (((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((q `1 ) ^2 ) / ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )) + (((q `2 ) ^2 ) / ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((q `1 ) ^2 ) / (1 + (((q `2 ) / (q `1 )) ^2 ))) + (((q `2 ) ^2 ) / ((sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))) ^2 )) by A9, SQUARE_1:def 4
.= (((q `1 ) ^2 ) / (1 + (((q `2 ) / (q `1 )) ^2 ))) + (((q `2 ) ^2 ) / (1 + (((q `2 ) / (q `1 )) ^2 ))) by A9, SQUARE_1:def 4
.= (((q `1 ) ^2 ) + ((q `2 ) ^2 )) / (1 + (((q `2 ) / (q `1 )) ^2 )) by XCMPLX_1:63
.= (((q `1 ) ^2 ) + ((q `2 ) ^2 )) / (1 + (((q `2 ) ^2 ) / ((q `1 ) ^2 ))) by XCMPLX_1:77
.= (((q `1 ) ^2 ) + ((q `2 ) ^2 )) / ((((q `1 ) ^2 ) / ((q `1 ) ^2 )) + (((q `2 ) ^2 ) / ((q `1 ) ^2 ))) by A12, XCMPLX_1:60
.= (((q `1 ) ^2 ) + ((q `2 ) ^2 )) / ((((q `1 ) ^2 ) + ((q `2 ) ^2 )) / ((q `1 ) ^2 )) by XCMPLX_1:63
.= ((q `1 ) ^2 ) * ((((q `1 ) ^2 ) + ((q `2 ) ^2 )) / (((q `1 ) ^2 ) + ((q `2 ) ^2 ))) by XCMPLX_1:82
.= ((q `1 ) ^2 ) * 1 by A10, COMPLEX1:2, XCMPLX_1:60
.= (q `1 ) ^2 ;
then |.|[((q `1 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `2 ) / (q `1 )) ^2 ))))]|.| <= 1 by A13, SQUARE_1:89;
hence ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| <= 1 ) by A2, A3, A7; :: thesis: verum

end;

case A14: ( q <> 0. (TOP-REAL 2) & not ( q `2 <= q `1 & - (q `1 ) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ; :: thesis: ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| <= 1 )

then A15: Sq_Circ . q = |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]| by JGRAPH_3:def 1;
A16: ( |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]| `1 = (q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) & |[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]| `2 = (q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ) by EUCLID:56;
A17: 1 + (((q `1 ) / (q `2 )) ^2 ) > 0 by XREAL_1:36, XREAL_1:65;
A18: q `2 <> 0 by A14;
then A19: (q `2 ) ^2 > 0 by SQUARE_1:74;
(q `2 ) ^2 <= 1 ^2 by A3, SQUARE_1:119;
then A20: sqrt ((q `2 ) ^2 ) <= 1 by A19, SQUARE_1:83, SQUARE_1:94;
|.|[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]|.| ^2 = (((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))) ^2 ) + (((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))) ^2 ) by A16, JGRAPH_3:10
.= (((q `1 ) ^2 ) / ((sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 )) + (((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((q `1 ) ^2 ) / ((sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 )) + (((q `2 ) ^2 ) / ((sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 )) by XCMPLX_1:77
.= (((q `1 ) ^2 ) / (1 + (((q `1 ) / (q `2 )) ^2 ))) + (((q `2 ) ^2 ) / ((sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))) ^2 )) by A17, SQUARE_1:def 4
.= (((q `1 ) ^2 ) / (1 + (((q `1 ) / (q `2 )) ^2 ))) + (((q `2 ) ^2 ) / (1 + (((q `1 ) / (q `2 )) ^2 ))) by A17, SQUARE_1:def 4
.= (((q `1 ) ^2 ) + ((q `2 ) ^2 )) / (1 + (((q `1 ) / (q `2 )) ^2 )) by XCMPLX_1:63
.= (((q `1 ) ^2 ) + ((q `2 ) ^2 )) / (1 + (((q `1 ) ^2 ) / ((q `2 ) ^2 ))) by XCMPLX_1:77
.= (((q `1 ) ^2 ) + ((q `2 ) ^2 )) / ((((q `1 ) ^2 ) / ((q `2 ) ^2 )) + (((q `2 ) ^2 ) / ((q `2 ) ^2 ))) by A19, XCMPLX_1:60
.= (((q `1 ) ^2 ) + ((q `2 ) ^2 )) / ((((q `1 ) ^2 ) + ((q `2 ) ^2 )) / ((q `2 ) ^2 )) by XCMPLX_1:63
.= ((q `2 ) ^2 ) * ((((q `1 ) ^2 ) + ((q `2 ) ^2 )) / (((q `1 ) ^2 ) + ((q `2 ) ^2 ))) by XCMPLX_1:82
.= ((q `2 ) ^2 ) * 1 by A18, COMPLEX1:2, XCMPLX_1:60
.= (q `2 ) ^2 ;
then |.|[((q `1 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 )))),((q `2 ) / (sqrt (1 + (((q `1 ) / (q `2 )) ^2 ))))]|.| <= 1 by A20, SQUARE_1:89;
hence ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| <= 1 ) by A2, A3, A15; :: thesis: verum

end;

end;

end;

hence y in Cb by A1; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Cb or y in Sq_Circ .: Kb )
assume y in Cb ; :: thesis: y in Sq_Circ .: Kb
then consider p2 being Point of (TOP-REAL 2) such that
A21: ( p2 = y & |.p2.| <= 1 ) by A1;
set q = p2;

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 A22: p2 = 0. (TOP-REAL 2) ; :: thesis: ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x )

then ( p2 `1 = 0 & p2 `2 = 0 ) by EUCLID:56, EUCLID:58;
then A23: y in Kb by A1, A21;
A24: (Sq_Circ " ) . y = y by A21, A22, JGRAPH_3:38;
A25: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
y = Sq_Circ . y by A21, A24, FUNCT_1:57, JGRAPH_3:54;
hence ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) by A23, A25; :: thesis: verum

end;

case A26: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ) ; :: thesis: ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x )

set px = |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]|;
A27: ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 = (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) & |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 = (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) by EUCLID:56;
1 + (((p2 `2 ) / (p2 `1 )) ^2 ) > 0 by XREAL_1:36, XREAL_1:65;
then A28: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by SQUARE_1:93;
A29: 1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ) > 0 by XREAL_1:36, XREAL_1:65;
A30: (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) = (p2 `2 ) / (p2 `1 ) by A27, A28, XCMPLX_1:92;
A31: p2 `1 = ((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A28, XCMPLX_1:90
.= (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by EUCLID:56 ;
A32: p2 `2 = ((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A28, XCMPLX_1:90
.= (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by EUCLID:56 ;
A33: |.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by JGRAPH_3:10;
A34: |.p2.| ^2 <= 1 ^2 by A21, SQUARE_1:77;

A35: now

assume ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 = 0 & |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 = 0 ) ; :: thesis: contradiction
then A36: ( (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 & (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 ) by EUCLID:56;
then A37: p2 `1 = 0 by A28, XCMPLX_1:6;
p2 `2 = 0 by A28, A36, XCMPLX_1:6;
hence contradiction by A26, A37, EUCLID:57, EUCLID:58; :: thesis: verum

end;

( ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) or ( p2 `2 >= p2 `1 & (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) ) by A26, A28, XREAL_1:66;
then A38: ( ( p2 `2 <= p2 `1 & (- (p2 `1 )) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) <= (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 >= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 & |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 <= - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ) ) by A27, A28, XREAL_1:66;
then ( ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 <= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 & - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) <= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 >= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 & |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 <= - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ) ) by A27, A28, XREAL_1:66;
then A39: Sq_Circ . |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| = |[((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) / (sqrt (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 )))),((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (sqrt (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))))]| by A35, JGRAPH_2:11, JGRAPH_3:def 1;
( ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 <= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 & - (- (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) >= - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 >= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 & |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 <= - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ) ) by A27, A28, A38, XREAL_1:26, XREAL_1:66;
then A40: ( ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 <= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 & |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 >= - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 >= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 & - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) >= - (- (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ) ) by XREAL_1:26;
A41: (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) / (sqrt (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) = p2 `1 by A27, A28, A30, XCMPLX_1:90;
A42: (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (sqrt (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) = p2 `2 by A27, A28, A30, XCMPLX_1:90;
A43: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
not |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 = 0 by A27, A28, A35, A38, XREAL_1:66;
then A44: (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 > 0 by SQUARE_1:74;
A45: (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 >= 0 by XREAL_1:65;
(((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) / ((sqrt (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) ^2 )) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (sqrt (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 )))) ^2 ) <= 1 by A30, A31, A32, A33, A34, XCMPLX_1:77;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) / ((sqrt (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) ^2 )) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) / ((sqrt (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) ^2 )) <= 1 by XCMPLX_1:77;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) / (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) / ((sqrt (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) ^2 )) <= 1 by A29, SQUARE_1:def 4;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) / (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) / (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) <= 1 by A29, SQUARE_1:def 4;
then ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) / (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) / (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 )))) * (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 )) <= 1 * (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 )) by A29, XREAL_1:66;
then ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) / (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) * (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) + ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) / (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) * (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) <= 1 * (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 )) ;
then ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) / (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) * (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 ))) <= 1 * (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 )) by A29, XCMPLX_1:88;
then A46: ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) <= 1 * (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 )) by A29, XCMPLX_1:88;
1 * (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) / (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 )) ^2 )) = 1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) / ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 )) by XCMPLX_1:77;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 )) - 1 <= (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) / ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ))) - 1 by A46, XREAL_1:11;
then ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 )) - 1) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) <= (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) / ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 )) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) by A44, XREAL_1:66;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) - 1)) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) <= (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 by A44, XCMPLX_1:88;
then A47: ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 )) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) * (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) - 1))) - ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) <= 0 by XREAL_1:49;
((((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 )) + ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 )) - (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) * 1))) - ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) = (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) - 1) * (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 )) ;
then ( ( ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) - 1 <= 0 & ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) - 1 >= 0 ) or ( ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) - 1 <= 0 & ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) >= 0 ) or ( ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) <= 0 & ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) - 1 >= 0 ) or ( ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) <= 0 & ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) >= 0 ) ) by A47, XREAL_1:131, XREAL_1:132;
then ( (((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) - 1) + 1 <= 0 + 1 & ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ^2 ) >= 0 ) by A44, A45, XREAL_1:9;
then A48: ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 <= 1 ^2 & |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 >= - (1 ^2 ) ) by SQUARE_1:117;
then ( ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 <= 1 & 1 >= - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 >= - 1 & - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) >= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 ) ) by A40, XXREAL_0:2;
then ( ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 <= 1 & - 1 <= - (- (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 )) ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 >= - 1 & - (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) >= - 1 ) ) by A48, XREAL_1:26, XXREAL_0:2;
then ( ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 <= 1 & - 1 <= |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 >= - 1 & - (- (|[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 )) <= - (- 1) ) ) by XREAL_1:26;
then |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| in Kb by A1, A48;
hence ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) by A21, A39, A41, A42, A43, EUCLID:57; :: thesis: verum

end;

case A49: ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1 ) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1 ) ) ) ; :: thesis: ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x )

set px = |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]|;
A50: ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2 ) ) ) ) by A49, JGRAPH_2:23;
A51: ( |[((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 ))) & |[((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 ))) ) by EUCLID:56;
1 + (((p2 `1 ) / (p2 `2 )) ^2 ) > 0 by XREAL_1:36, XREAL_1:65;
then A52: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by SQUARE_1:93;
A53: 1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ) > 0 by XREAL_1:36, XREAL_1:65;
A54: (|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) = (p2 `1 ) / (p2 `2 ) by A51, A52, XCMPLX_1:92;
A55: p2 `2 = ((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A52, XCMPLX_1:90
.= (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by EUCLID:56 ;
A56: p2 `1 = ((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A52, XCMPLX_1:90
.= (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by EUCLID:56 ;
A57: |.p2.| ^2 = ((p2 `2 ) ^2 ) + ((p2 `1 ) ^2 ) by JGRAPH_3:10;
A58: |.p2.| ^2 <= 1 ^2 by A21, SQUARE_1:77;

A59: now

assume ( |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 = 0 & |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 = 0 ) ; :: thesis: contradiction
then A60: ( (p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = 0 & (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = 0 ) by EUCLID:56;
then p2 `1 = 0 by A52, XCMPLX_1:6;
hence contradiction by A49, A52, A60, XCMPLX_1:6; :: thesis: verum

end;

( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) <= (- (p2 `2 )) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) ) by A50, A52, XREAL_1:66;
then A61: ( ( p2 `1 <= p2 `2 & (- (p2 `2 )) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) <= (p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) ) or ( |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 & |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ) ) by A51, A52, XREAL_1:66;
then ( ( |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 & - (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) <= |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) or ( |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 & |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ) ) by A51, A52, XREAL_1:66;
then A62: Sq_Circ . |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (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 ))))]| `1 ) / (sqrt (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 )))),((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) / (sqrt (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))))]| by A59, JGRAPH_2:11, JGRAPH_3:14;
( ( |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 & - (- (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) >= - (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ) or ( |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 & |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ) ) by A51, A52, A61, XREAL_1:26, XREAL_1:66;
then A63: ( ( |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 & |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 >= - (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ) or ( |[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 & - (|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ) ) by XREAL_1:26;
A64: (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) / (sqrt (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) = p2 `2 by A51, A52, A54, XCMPLX_1:90;
A65: (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) / (sqrt (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) = p2 `1 by A51, A52, A54, XCMPLX_1:90;
A66: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
not |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 = 0 by A51, A52, A59, A61, XREAL_1:66;
then A67: (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 > 0 by SQUARE_1:74;
A68: (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 >= 0 by XREAL_1:65;
(((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) / ((sqrt (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) ^2 )) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) / (sqrt (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 )))) ^2 ) <= 1 by A54, A55, A56, A57, A58, XCMPLX_1:77;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) / ((sqrt (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) ^2 )) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) / ((sqrt (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) ^2 )) <= 1 by XCMPLX_1:77;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) / (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) / ((sqrt (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) ^2 )) <= 1 by A53, SQUARE_1:def 4;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) / (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) / (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) <= 1 by A53, SQUARE_1:def 4;
then ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) / (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) / (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 )))) * (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 )) <= 1 * (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 )) by A53, XREAL_1:66;
then ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) / (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) * (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) + ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) / (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) * (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) <= 1 * (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 )) ;
then ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) + ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) / (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) * (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 ))) <= 1 * (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 )) by A53, XCMPLX_1:88;
then A69: ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) <= 1 * (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 )) by A53, XCMPLX_1:88;
1 * (1 + (((|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 )) ^2 )) = 1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) / ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 )) by XCMPLX_1:77;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 )) - 1 <= (1 + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) / ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ))) - 1 by A69, XREAL_1:11;
then ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 )) - 1) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) <= (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) / ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 )) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) by A67, XREAL_1:66;
then (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) - 1)) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) <= (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 by A67, XCMPLX_1:88;
then A70: ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 )) + (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) * (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) - 1))) - ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) <= 0 by XREAL_1:49;
((((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 )) + ((((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) * ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 )) - (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) * 1))) - ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) = (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) - 1) * (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 )) ;
then ( ( ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) - 1 <= 0 or ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) <= 0 ) & ( ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) - 1 >= 0 or ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) >= 0 ) ) by A70, XREAL_1:131, XREAL_1:132;
then ( (((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) - 1) + 1 <= 0 + 1 & ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) + ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ^2 ) >= 0 ) by A67, A68, XREAL_1:9;
then A71: ( |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 <= 1 ^2 & |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 >= - (1 ^2 ) ) by SQUARE_1:117;
then ( ( |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 <= 1 & 1 >= - (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 >= - 1 & - (|[((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 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ) by A63, XXREAL_0:2;
then ( ( |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 <= 1 & - 1 <= - (- (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 )) ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 >= - 1 & - (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) >= - 1 ) ) by A71, XREAL_1:26, XXREAL_0:2;
then ( ( |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 <= 1 & - 1 <= |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 ) or ( |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 >= - 1 & - (- (|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 )) <= - (- 1) ) ) by XREAL_1:26;
then |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| in Kb by A1, A71;
hence ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) by A21, A62, A64, A65, A66, EUCLID:57; :: thesis: verum

end;

end;

end;

hence y in Sq_Circ .: Kb by FUNCT_1:def 12; :: thesis: verum