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 object ; :: 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 object such that
x in dom Sq_Circ and
A2: x in Kb and
A3: y = Sq_Circ . x by FUNCT_1:def 6;
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 :: thesis: ( ( q = 0. (TOP-REAL 2) & contradiction ) or ( q <> 0. (TOP-REAL 2) & ( ( q `2 <= q `1 & - (q `1) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1) ) ) & ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| > 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) ) & ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| > 1 ) ) )
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 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: ( ( - 1 <= q `2 & q `2 <= 1 ) or - 1 > q `1 or q `1 > 1 )
proof
assume A9: ( not - 1 <= q `2 or not q `2 <= 1 ) ; :: thesis: ( - 1 > q `1 or q `1 > 1 )
now :: thesis: ( ( - 1 > q `2 & ( - 1 > q `1 or q `1 > 1 ) ) or ( q `2 > 1 & ( - 1 > q `1 or q `1 > 1 ) ) )
per cases ( - 1 > q `2 or q `2 > 1 ) by A9;
case A10: - 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 A6, XXREAL_0:2;
hence ( - 1 > q `1 or q `1 > 1 ) by A10, XREAL_1:24, 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 A6, XXREAL_0:2;
then ( 1 < q `1 or - (- (q `1)) < - 1 ) by XREAL_1:24;
hence ( - 1 > q `1 or q `1 > 1 ) ; :: thesis: verum
end;
end;
end;
hence ( - 1 > q `1 or q `1 > 1 ) ; :: thesis: verum
end;
A11: |[((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:52;
A12: |[((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:52;
A13: 1 + (((q `2) / (q `1)) ^2) > 0 by XREAL_1:34, XREAL_1:63;
then A16: (q `1) ^2 > 0 by SQUARE_1:12;
(q `1) ^2 > 1 ^2 by A5, A8, SQUARE_1:47;
then A17: sqrt ((q `1) ^2) > 1 by SQUARE_1:18, SQUARE_1:27;
|.|[((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 A11, A12, JGRAPH_3:1
.= (((q `1) ^2) / ((sqrt (1 + (((q `2) / (q `1)) ^2))) ^2)) + (((q `2) / (sqrt (1 + (((q `2) / (q `1)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((q `1) ^2) / (1 + (((q `2) / (q `1)) ^2))) + (((q `2) ^2) / ((sqrt (1 + (((q `2) / (q `1)) ^2))) ^2)) by A13, SQUARE_1:def 2
.= (((q `1) ^2) / (1 + (((q `2) / (q `1)) ^2))) + (((q `2) ^2) / (1 + (((q `2) / (q `1)) ^2))) by A13, SQUARE_1:def 2
.= (((q `1) ^2) + ((q `2) ^2)) / (1 + (((q `2) / (q `1)) ^2)) by XCMPLX_1:62
.= (((q `1) ^2) + ((q `2) ^2)) / (1 + (((q `2) ^2) / ((q `1) ^2))) by XCMPLX_1:76
.= (((q `1) ^2) + ((q `2) ^2)) / ((((q `1) ^2) / ((q `1) ^2)) + (((q `2) ^2) / ((q `1) ^2))) by A16, XCMPLX_1:60
.= (((q `1) ^2) + ((q `2) ^2)) / ((((q `1) ^2) + ((q `2) ^2)) / ((q `1) ^2)) by XCMPLX_1:62
.= ((q `1) ^2) * ((((q `1) ^2) + ((q `2) ^2)) / (((q `1) ^2) + ((q `2) ^2))) by XCMPLX_1:81
.= ((q `1) ^2) * 1 by A14, COMPLEX1:1, 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 A17, SQUARE_1:22;
hence ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| > 1 ) by A3, A4, A7; :: thesis: verum
end;
case A18: ( 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 A19: 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;
A20: |[((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:52;
A21: |[((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:52;
A22: 1 + (((q `1) / (q `2)) ^2) > 0 by XREAL_1:34, XREAL_1:63;
A23: q `2 <> 0 by A18;
then A24: (q `2) ^2 > 0 by SQUARE_1:12;
( ( - 1 <= q `1 & q `1 <= 1 ) or - 1 > q `2 or q `2 > 1 )
proof
assume A25: ( not - 1 <= q `1 or not q `1 <= 1 ) ; :: thesis: ( - 1 > q `2 or q `2 > 1 )
now :: thesis: ( ( - 1 > q `1 & ( - 1 > q `2 or q `2 > 1 ) ) or ( q `1 > 1 & ( - 1 > q `2 or q `2 > 1 ) ) )
per cases ( - 1 > q `1 or q `1 > 1 ) by A25;
case A26: - 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 A18, XREAL_1:24, XXREAL_0:2;
then ( - (q `2) < - 1 or - 1 > q `2 ) by A26, XXREAL_0:2;
hence ( - 1 > q `2 or q `2 > 1 ) by XREAL_1:24; :: thesis: verum
end;
case A27: 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 A18, XREAL_1:24;
then ( 1 < - (q `2) or ( q `2 > q `1 & q `2 > - (q `1) ) ) by A27, XXREAL_0:2;
then ( - 1 > - (- (q `2)) or 1 < q `2 ) by A27, XREAL_1:24, 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:47;
then A28: sqrt ((q `2) ^2) > 1 by SQUARE_1:18, SQUARE_1:27;
|.|[((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 A20, A21, JGRAPH_3:1
.= (((q `1) ^2) / ((sqrt (1 + (((q `1) / (q `2)) ^2))) ^2)) + (((q `2) / (sqrt (1 + (((q `1) / (q `2)) ^2)))) ^2) by XCMPLX_1:76
.= (((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:76
.= (((q `1) ^2) / (1 + (((q `1) / (q `2)) ^2))) + (((q `2) ^2) / ((sqrt (1 + (((q `1) / (q `2)) ^2))) ^2)) by A22, SQUARE_1:def 2
.= (((q `1) ^2) / (1 + (((q `1) / (q `2)) ^2))) + (((q `2) ^2) / (1 + (((q `1) / (q `2)) ^2))) by A22, SQUARE_1:def 2
.= (((q `1) ^2) + ((q `2) ^2)) / (1 + (((q `1) / (q `2)) ^2)) by XCMPLX_1:62
.= (((q `1) ^2) + ((q `2) ^2)) / (1 + (((q `1) ^2) / ((q `2) ^2))) by XCMPLX_1:76
.= (((q `1) ^2) + ((q `2) ^2)) / ((((q `1) ^2) / ((q `2) ^2)) + (((q `2) ^2) / ((q `2) ^2))) by A24, XCMPLX_1:60
.= (((q `1) ^2) + ((q `2) ^2)) / ((((q `1) ^2) + ((q `2) ^2)) / ((q `2) ^2)) by XCMPLX_1:62
.= ((q `2) ^2) * ((((q `1) ^2) + ((q `2) ^2)) / (((q `1) ^2) + ((q `2) ^2))) by XCMPLX_1:81
.= ((q `2) ^2) * 1 by A23, COMPLEX1:1, 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 A28, SQUARE_1:22;
hence ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| > 1 ) by A3, A4, A19; :: thesis: verum
end;
end;
end;
hence y in Cb by A1; :: thesis: verum
end;
let y be object ; :: 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
A29: p2 = y and
A30: |.p2.| > 1 by A1;
set q = p2;
now :: thesis: ( ( p2 = 0. (TOP-REAL 2) & contradiction ) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) & ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) & ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) ) )
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 A31: ( 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))))]|;
A32: |[((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:52;
A33: |[((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:52;
1 + (((p2 `2) / (p2 `1)) ^2) > 0 by XREAL_1:34, XREAL_1:63;
then A34: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0 by SQUARE_1:25;
A35: 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:34, XREAL_1:63;
A36: (|[((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 A32, A33, A34, XCMPLX_1:91;
A37: p2 `1 = ((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A34, XCMPLX_1:89
.= (|[((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:52 ;
A38: p2 `2 = ((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by A34, XCMPLX_1:89
.= (|[((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:52 ;
A39: |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
A40: |.p2.| ^2 > 1 ^2 by A30, SQUARE_1:16;
A41: now :: thesis: ( |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 = 0 implies not |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 = 0 )
assume that
A42: |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 = 0 and
A43: |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 = 0 ; :: thesis: contradiction
A44: (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) = 0 by A42, EUCLID:52;
A45: (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) = 0 by A43, EUCLID:52;
A46: p2 `1 = 0 by A34, A44, XCMPLX_1:6;
p2 `2 = 0 by A34, A45, XCMPLX_1:6;
hence contradiction by A31, A46, EUCLID:53, EUCLID:54; :: 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 A31, A34, XREAL_1:64;
then A47: ( ( 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 A32, A33, A34, XREAL_1:64;
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 A32, A33, A34, XREAL_1:64;
then A48: 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 A41, JGRAPH_2:3, JGRAPH_3:def 1;
A49: (|[((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 A32, A34, A36, XCMPLX_1:89;
A50: (|[((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 A33, A34, A36, XCMPLX_1:89;
A51: 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 A32, A33, A34, A41, A47, XREAL_1:64;
then A52: (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2 > 0 by SQUARE_1:12;
A53: (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2 >= 0 by XREAL_1:63;
(((|[((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 A36, A37, A38, A39, A40, XCMPLX_1:76;
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:76;
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 A35, SQUARE_1:def 2;
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 A35, SQUARE_1:def 2;
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 A35, XREAL_1:68;
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 A35, XCMPLX_1:87;
then A54: ((|[((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 A35, XCMPLX_1:87;
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:76;
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 A54, XREAL_1:9;
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 A52, XREAL_1:68;
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) - 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 A52, XCMPLX_1:87;
((((|[((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 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 ) by A55, XREAL_1:50;
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 A52, A53, XREAL_1:6;
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:49;
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 A29, A48, A49, A50, A51, EUCLID:53; :: thesis: verum
end;
case A56: ( 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))))]|;
A57: ( ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) ) ) by A56, JGRAPH_2:13;
A58: |[((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:52;
A59: |[((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:52;
1 + (((p2 `1) / (p2 `2)) ^2) > 0 by XREAL_1:34, XREAL_1:63;
then A60: sqrt (1 + (((p2 `1) / (p2 `2)) ^2)) > 0 by SQUARE_1:25;
A61: 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:34, XREAL_1:63;
A62: (|[((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 A58, A59, A60, XCMPLX_1:91;
A63: p2 `2 = ((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) by A60, XCMPLX_1:89
.= (|[((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:52 ;
A64: p2 `1 = ((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) by A60, XCMPLX_1:89
.= (|[((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:52 ;
A65: |.p2.| ^2 = ((p2 `2) ^2) + ((p2 `1) ^2) by JGRAPH_3:1;
A66: |.p2.| ^2 > 1 ^2 by A30, SQUARE_1:16;
A67: now :: thesis: ( |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 = 0 implies not |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 = 0 )
assume that
A68: |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 = 0 and
A69: |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 = 0 ; :: thesis: contradiction
A70: (p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) = 0 by A68, EUCLID:52;
(p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) = 0 by A69, EUCLID:52;
then p2 `1 = 0 by A60, XCMPLX_1:6;
hence contradiction by A56, A70; :: 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 A57, A60, XREAL_1:64;
then A71: ( ( 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 A58, A59, A60, XREAL_1:64;
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 A58, A59, A60, XREAL_1:64;
then A72: 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 A67, JGRAPH_2:3, JGRAPH_3:4;
A73: (|[((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 A58, A60, A62, XCMPLX_1:89;
A74: (|[((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 A59, A60, A62, XCMPLX_1:89;
A75: 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 A58, A59, A60, A67, A71, XREAL_1:64;
then A76: (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2 > 0 by SQUARE_1:12;
A77: (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ^2 >= 0 by XREAL_1:63;
(((|[((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 A62, A63, A64, A65, A66, XCMPLX_1:76;
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:76;
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 A61, SQUARE_1:def 2;
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 A61, SQUARE_1:def 2;
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 A61, XREAL_1:68;
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 A61, XCMPLX_1:87;
then A78: ((|[((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 A61, XCMPLX_1:87;
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:76;
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 A78, XREAL_1:9;
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 A76, XREAL_1:68;
then A79: (((|[((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 A76, XCMPLX_1:87;
((((|[((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))))]| `1) ^2) + ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) < 0 ) by A79, XREAL_1:50;
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 A76, A77, XREAL_1:6;
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:49;
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 A29, A72, A73, A74, A75, EUCLID:53; :: thesis: verum
end;
end;
end;
hence y in Sq_Circ .: Kb by FUNCT_1:def 6; :: thesis: verum