let Kb, Cb be Subset of (TOP-REAL 2); :: thesis: ( Kb = { p where p is Point of (TOP-REAL 2) : ( not - 1 < p `1 or not p `1 < 1 or not - 1 < p `2 or not 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) : ( not - 1 < p `1 or not p `1 < 1 or not - 1 < p `2 or not 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
x in dom Sq_Circ and
A2: x in Kb and
A3: y = Sq_Circ . x by FUNCT_1:def 12;
consider q being Point of (TOP-REAL 2) such that
A4: q = x and
A5: ( not - 1 < q `1 or not q `1 < 1 or not - 1 < q `2 or not 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 A8: ( 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 A9: 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;
A10: ( ( - 1 < q `2 & q `2 < 1 ) or - 1 >= q `1 or q `1 >= 1 )
proof
assume A11: ( not - 1 < q `2 or not q `2 < 1 ) ; :: thesis: ( - 1 >= q `1 or q `1 >= 1 )
now
per cases ( - 1 >= q `2 or q `2 >= 1 ) by A11;
case A12: - 1 >= q `2 ; :: thesis: ( - 1 >= q `1 or q `1 >= 1 )
then ( - (q `1 ) <= - 1 or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) by A8, XXREAL_0:2;
hence ( - 1 >= q `1 or q `1 >= 1 ) by A12, XREAL_1:26, XXREAL_0:2; :: thesis: verum
end;
case q `2 >= 1 ; :: thesis: ( - 1 >= q `1 or q `1 >= 1 )
then ( 1 <= q `1 or 1 <= - (q `1 ) ) by A8, XXREAL_0:2;
then ( 1 <= q `1 or - (- (q `1 )) <= - 1 ) by XREAL_1:26;
hence ( - 1 >= q `1 or q `1 >= 1 ) ; :: thesis: verum
end;
end;
end;
hence ( - 1 >= q `1 or q `1 >= 1 ) ; :: thesis: verum
end;
A13: |[((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 ))) by EUCLID:56;
A14: |[((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;
A15: 1 + (((q `2 ) / (q `1 )) ^2 ) > 0 by XREAL_1:36, XREAL_1:65;
then A18: (q `1 ) ^2 > 0 by SQUARE_1:74;
(q `1 ) ^2 >= 1 ^2 by A5, A10, SQUARE_1:118;
then A19: sqrt ((q `1 ) ^2 ) >= 1 by 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 A13, A14, 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 A15, SQUARE_1:def 4
.= (((q `1 ) ^2 ) / (1 + (((q `2 ) / (q `1 )) ^2 ))) + (((q `2 ) ^2 ) / (1 + (((q `2 ) / (q `1 )) ^2 ))) by A15, 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 A18, 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 A16, 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 A19, SQUARE_1:89;
hence ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| >= 1 ) by A3, A4, A9; :: thesis: verum
end;
case A20: ( 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 A21: 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;
A22: |[((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 ))) by EUCLID:56;
A23: |[((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;
A24: 1 + (((q `1 ) / (q `2 )) ^2 ) > 0 by XREAL_1:36, XREAL_1:65;
A25: q `2 <> 0 by A20;
then A26: (q `2 ) ^2 > 0 by SQUARE_1:74;
( ( - 1 < q `1 & q `1 < 1 ) or - 1 >= q `2 or q `2 >= 1 )
proof
assume A27: ( not - 1 < q `1 or not q `1 < 1 ) ; :: thesis: ( - 1 >= q `2 or q `2 >= 1 )
now
per cases ( - 1 >= q `1 or q `1 >= 1 ) by A27;
case A28: - 1 >= q `1 ; :: thesis: ( - 1 >= q `2 or q `2 >= 1 )
then ( q `2 <= - 1 or ( q `1 < q `2 & - (q `2 ) <= - (- (q `1 )) ) ) by A20, XREAL_1:26, XXREAL_0:2;
then ( - (q `2 ) <= - 1 or - 1 >= q `2 ) by A28, XXREAL_0:2;
hence ( - 1 >= q `2 or q `2 >= 1 ) by XREAL_1:26; :: thesis: verum
end;
case A29: q `1 >= 1 ; :: thesis: ( - 1 >= q `2 or q `2 >= 1 )
( ( - (- (q `1 )) <= - (q `2 ) & q `2 <= q `1 ) or ( q `2 >= q `1 & q `2 >= - (q `1 ) ) ) by A20, XREAL_1:26;
then ( 1 <= - (q `2 ) or ( q `2 >= q `1 & q `2 >= - (q `1 ) ) ) by A29, XXREAL_0:2;
then ( - 1 >= - (- (q `2 )) or 1 <= q `2 ) by A29, XREAL_1:26, XXREAL_0:2;
hence ( - 1 >= q `2 or q `2 >= 1 ) ; :: thesis: verum
end;
end;
end;
hence ( - 1 >= q `2 or q `2 >= 1 ) ; :: thesis: verum
end;
then (q `2 ) ^2 >= 1 ^2 by A5, SQUARE_1:118;
then A30: sqrt ((q `2 ) ^2 ) >= 1 by 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 A22, A23, 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 A24, SQUARE_1:def 4
.= (((q `1 ) ^2 ) / (1 + (((q `1 ) / (q `2 )) ^2 ))) + (((q `2 ) ^2 ) / (1 + (((q `1 ) / (q `2 )) ^2 ))) by A24, 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 A26, 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 A25, 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 A30, SQUARE_1:89;
hence ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| >= 1 ) by A3, A4, A21; :: 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
A31: p2 = y and
A32: |.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 A33: ( 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 ))))]|;
A34: |[((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 ))) by EUCLID:56;
A35: |[((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 A36: sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )) > 0 by SQUARE_1:93;
A37: 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;
A38: (|[((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 A34, A35, A36, XCMPLX_1:92;
A39: p2 `1 = ((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A36, 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 ;
A40: p2 `2 = ((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) by A36, 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 ;
A41: |.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by JGRAPH_3:10;
A42: |.p2.| ^2 >= 1 ^2 by A32, SQUARE_1:77;
A43: now
assume that
A44: |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 = 0 and
A45: |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `2 = 0 ; :: thesis: contradiction
A46: (p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 by A44, EUCLID:56;
A47: (p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))) = 0 by A45, EUCLID:56;
A48: p2 `1 = 0 by A36, A46, XCMPLX_1:6;
p2 `2 = 0 by A36, A47, XCMPLX_1:6;
hence contradiction by A33, A48, 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 A33, A36, XREAL_1:66;
then A49: ( ( 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 A34, A35, A36, 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 A34, A35, A36, XREAL_1:66;
then A50: 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 A43, JGRAPH_2:11, JGRAPH_3:def 1;
A51: (|[((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 A34, A36, A38, XCMPLX_1:90;
A52: (|[((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 A35, A36, A38, XCMPLX_1:90;
A53: 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 A34, A35, A36, A43, A49, XREAL_1:66;
then A54: (|[((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;
then A55: ((|[((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 XREAL_1:36, 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 A38, A39, A40, A41, A42, 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 A37, 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 A37, 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 A37, 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 A37, XCMPLX_1:88;
then A56: ((|[((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 A37, 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 A56, 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 A54, 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 A54, XCMPLX_1:88;
then A57: ((((|[((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:50;
((((|[((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 by A55, A57, XREAL_1:134;
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 by XREAL_1:9;
then ( |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 >= 1 ^2 or |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| `1 <= - 1 ) by SQUARE_1:120;
then |[((p2 `1 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| in Kb by A1;
hence ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) by A31, A50, A51, A52, A53, EUCLID:57; :: thesis: verum
end;
case A58: ( 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 ))))]|;
A59: ( ( p2 `1 <= p2 `2 & - (p2 `2 ) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2 ) ) ) by A58, JGRAPH_2:23;
A60: |[((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;
A61: |[((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 A62: sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )) > 0 by SQUARE_1:93;
A63: 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;
A64: (|[((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 A60, A61, A62, XCMPLX_1:92;
A65: p2 `2 = ((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A62, 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 ;
A66: p2 `1 = ((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) by A62, 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 ;
A67: |.p2.| ^2 = ((p2 `2 ) ^2 ) + ((p2 `1 ) ^2 ) by JGRAPH_3:10;
A68: |.p2.| ^2 >= 1 ^2 by A32, SQUARE_1:77;
A69: now
assume that
A70: |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 = 0 and
A71: |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `1 = 0 ; :: thesis: contradiction
A72: (p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = 0 by A70, EUCLID:56;
(p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))) = 0 by A71, EUCLID:56;
then p2 `1 = 0 by A62, XCMPLX_1:6;
hence contradiction by A58, A62, A72, 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 A59, A62, XREAL_1:66;
then A73: ( ( 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 A60, A61, A62, 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 A60, A61, A62, XREAL_1:66;
then A74: 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 A69, JGRAPH_2:11, JGRAPH_3:14;
A75: (|[((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 A60, A62, A64, XCMPLX_1:90;
A76: (|[((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 A61, A62, A64, XCMPLX_1:90;
A77: 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 A60, A61, A62, A69, A73, XREAL_1:66;
then A78: (|[((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;
A79: (|[((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 A64, A65, A66, A67, A68, 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 A63, 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 A63, 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 A63, 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 A63, XCMPLX_1:88;
then A80: ((|[((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 A63, 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 A80, 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 A78, 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 A78, XCMPLX_1:88;
then A81: ((((|[((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:50;
((((|[((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 & ((|[((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 ) >= 0 ) or ( ((|[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 ) ^2 ) - 1 <= 0 & ((|[((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 ) <= 0 ) ) by A81, XREAL_1:134;
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 by A78, A79, XREAL_1:9;
then ( |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 >= 1 ^2 or |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| `2 <= - 1 ) by SQUARE_1:120;
then |[((p2 `1 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) * (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| in Kb by A1;
hence ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) by A31, A74, A75, A76, A77, EUCLID:57; :: thesis: verum
end;
end;
end;
hence y in Sq_Circ .: Kb by FUNCT_1:def 12; :: thesis: verum