let Kb, Cb be Subset of (); :: thesis: ( Kb = { p where p is Point of () : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & Cb = { p2 where p2 is Point of () : |.p2.| < 1 } implies Sq_Circ .: Kb = Cb )
assume A1: ( Kb = { p where p is Point of () : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & Cb = { p2 where p2 is Point of () : |.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 () such that
A4: q = x and
A5: - 1 < q `1 and
A6: q `1 < 1 and
A7: - 1 < q `2 and
A8: q `2 < 1 by A1, A2;
now :: thesis: ( ( q = 0. () & ex p2 being Point of () st
( p2 = y & |.p2.| < 1 ) ) or ( q <> 0. () & ( ( q `2 <= q `1 & - (q `1) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1) ) ) & ex p2 being Point of () st
( p2 = y & |.p2.| < 1 ) ) or ( q <> 0. () & not ( q `2 <= q `1 & - (q `1) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1) ) & ex p2 being Point of () st
( p2 = y & |.p2.| < 1 ) ) )
per cases ( q = 0. () or ( q <> 0. () & ( ( q `2 <= q `1 & - (q `1) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1) ) ) ) or ( q <> 0. () & not ( q `2 <= q `1 & - (q `1) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1) ) ) ) ;
case A9: q = 0. () ; :: thesis: ex p2 being Point of () st
( p2 = y & |.p2.| < 1 )

then A10: Sq_Circ . q = q by JGRAPH_3:def 1;
|.q.| = 0 by ;
hence ex p2 being Point of () st
( p2 = y & |.p2.| < 1 ) by A3, A4, A10; :: thesis: verum
end;
case A11: ( q <> 0. () & ( ( q `2 <= q `1 & - (q `1) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1) ) ) ) ; :: thesis: ex p2 being Point of () st
( p2 = y & |.p2.| < 1 )

then A12: 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;
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:52;
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:52;
A15: 1 + (((q `2) / (q `1)) ^2) > 0 by ;
then A18: (q `1) ^2 > 0 by SQUARE_1:12;
(q `1) ^2 < 1 ^2 by ;
then A19: sqrt ((q `1) ^2) < 1 by ;
|.|[((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
.= (((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
.= (((q `1) ^2) / (1 + (((q `2) / (q `1)) ^2))) + (((q `2) ^2) / (1 + (((q `2) / (q `1)) ^2))) by
.= (((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
.= (((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
.= (q `1) ^2 ;
then |.|[((q `1) / (sqrt (1 + (((q `2) / (q `1)) ^2)))),((q `2) / (sqrt (1 + (((q `2) / (q `1)) ^2))))]|.| < 1 by ;
hence ex p2 being Point of () st
( p2 = y & |.p2.| < 1 ) by A3, A4, A12; :: thesis: verum
end;
case A20: ( q <> 0. () & not ( q `2 <= q `1 & - (q `1) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1) ) ) ; :: thesis: ex p2 being Point of () 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:52;
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:52;
A24: 1 + (((q `1) / (q `2)) ^2) > 0 by ;
A25: q `2 <> 0 by A20;
then A26: (q `2) ^2 > 0 by SQUARE_1:12;
(q `2) ^2 < 1 ^2 by ;
then A27: sqrt ((q `2) ^2) < 1 by ;
|.|[((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
.= (((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
.= (((q `1) ^2) / (1 + (((q `1) / (q `2)) ^2))) + (((q `2) ^2) / (1 + (((q `1) / (q `2)) ^2))) by
.= (((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
.= (((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
.= (q `2) ^2 ;
then |.|[((q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) / (sqrt (1 + (((q `1) / (q `2)) ^2))))]|.| < 1 by ;
hence ex p2 being Point of () 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 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 () such that
A28: p2 = y and
A29: |.p2.| < 1 by A1;
set q = p2;
now :: thesis: ( ( p2 = 0. () & ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) ) or ( p2 <> 0. () & ( ( 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. () & 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. () or ( p2 <> 0. () & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) ) or ( p2 <> 0. () & not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) ) ;
case A30: p2 = 0. () ; :: thesis: ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x )

then A31: p2 `1 = 0 by ;
p2 `2 = 0 by ;
then A32: y in Kb by A1, A28, A31;
A33: (Sq_Circ ") . y = y by ;
A34: dom Sq_Circ = the carrier of () by FUNCT_2:def 1;
y = Sq_Circ . y by ;
hence ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) by ; :: thesis: verum
end;
case A35: ( p2 <> 0. () & ( ( 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))))]|;
A36: |[((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;
A37: |[((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 ;
then A38: sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0 by SQUARE_1:25;
A39: 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 ;
A40: (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) / (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) = (p2 `2) / (p2 `1) by ;
A41: p2 `1 = ((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by
.= (|[((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 ;
A42: p2 `2 = ((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) by
.= (|[((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 ;
A43: |.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
A44: |.p2.| ^2 < 1 ^2 by ;
A45: 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
A46: |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 = 0 and
A47: |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 = 0 ; :: thesis: contradiction
A48: (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) = 0 by ;
A49: (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) = 0 by ;
A50: p2 `1 = 0 by ;
p2 `2 = 0 by ;
hence contradiction by A35, A50, 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 ;
then A51: ( ( 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 ;
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 ;
then A52: 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 ;
( ( |[((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 ;
then A53: ( ( |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 <= |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 & |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 >= - (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ) or ( |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 >= |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 & - (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) >= - (- (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1)) ) ) by XREAL_1:24;
A54: (|[((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 ;
A55: (|[((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 ;
A56: dom Sq_Circ = the carrier of () 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 ;
then A57: (|[((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;
A58: (|[((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 ;
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 ;
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 ;
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 ;
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 ;
then A59: ((|[((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 ;
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 ;
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 ;
then A60: (((|[((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 ;
((((|[((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 ;
then A61: (((|[((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 ;
then A62: |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 < 1 ^2 by SQUARE_1:48;
A63: |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 > - (1 ^2) by ;
( ( |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 < 1 & 1 > - (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ) or ( |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 >= |[((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 ;
then ( ( |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 < 1 & - 1 < - (- (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2)) ) or ( |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 > - 1 & - (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) > - 1 ) ) by ;
then ( ( |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 < 1 & - 1 < |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 ) or ( |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 > - 1 & - (- (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2)) < - (- 1) ) ) by XREAL_1:24;
then |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| in Kb by A1, A62, A63;
hence ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) by ; :: thesis: verum
end;
case A64: ( p2 <> 0. () & 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))))]|;
A65: ( ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) ) ) by ;
A66: |[((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;
A67: |[((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 ;
then A68: sqrt (1 + (((p2 `1) / (p2 `2)) ^2)) > 0 by SQUARE_1:25;
A69: 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 ;
A70: (|[((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 ;
A71: p2 `2 = ((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) by
.= (|[((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 ;
A72: p2 `1 = ((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) by
.= (|[((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 ;
A73: |.p2.| ^2 = ((p2 `2) ^2) + ((p2 `1) ^2) by JGRAPH_3:1;
A74: |.p2.| ^2 < 1 ^2 by ;
A75: 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
A76: |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 = 0 and
A77: |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 = 0 ; :: thesis: contradiction
A78: (p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) = 0 by ;
(p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))) = 0 by ;
then p2 `1 = 0 by ;
hence contradiction by A64, A68, A78, 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 ;
then A79: ( ( 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 ;
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 ;
then A80: 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 ;
( ( |[((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 ;
then A81: ( ( |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 <= |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 & |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 >= - (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ) or ( |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 >= |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 & - (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) >= - (- (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2)) ) ) by XREAL_1:24;
A82: (|[((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 ;
A83: (|[((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 ;
A84: dom Sq_Circ = the carrier of () 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 ;
then A85: (|[((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;
A86: (|[((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 ;
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 ;
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 ;
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 ;
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 ;
then A87: ((|[((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 ;
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 ;
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 ;
then A88: (((|[((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 ;
((((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) * ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2)) + ((((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) * ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ^2)) - (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) * 1))) - ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ^2) = (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) - 1) * (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) + ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ^2)) ;
then ( ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) - 1 < 0 or ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) + ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ^2) < 0 ) by ;
then A89: (((|[((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 ;
then A90: |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 < 1 ^2 by SQUARE_1:48;
A91: |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 > - (1 ^2) by ;
( ( |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 < 1 & 1 > - (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ) or ( |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 >= |[((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 ;
then ( ( |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 < 1 & - 1 < - (- (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1)) ) or ( |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 > - 1 & - (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) > - 1 ) ) by ;
then ( ( |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 < 1 & - 1 < |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 ) or ( |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 > - 1 & - (- (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1)) < - (- 1) ) ) by XREAL_1:24;
then |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| in Kb by A1, A90, A91;
hence ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) by ; :: thesis: verum
end;
end;
end;
hence y in Sq_Circ .: Kb by FUNCT_1:def 6; :: thesis: verum