let Kb, Cb be Subset of (TOP-REAL 2); ( Kb = { p where p is Point of (TOP-REAL 2) : ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| <= 1 } implies Sq_Circ .: Kb = Cb )
assume A1:
( Kb = { p where p is Point of (TOP-REAL 2) : ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| <= 1 } )
; Sq_Circ .: Kb = Cb
thus
Sq_Circ .: Kb c= Cb
XBOOLE_0:def 10 Cb c= Sq_Circ .: Kbproof
let y be
object ;
TARSKI:def 3 ( not y in Sq_Circ .: Kb or y in Cb )
assume
y in Sq_Circ .: Kb
;
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:
- 1
<= q `1
and A6:
q `1 <= 1
and A7:
- 1
<= q `2
and A8:
q `2 <= 1
by A1, A2;
now ( ( q = 0. (TOP-REAL 2) & ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| <= 1 ) ) 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 A11:
(
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 )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 XREAL_1:34, XREAL_1:63;
then A18:
(q `1) ^2 > 0
by SQUARE_1:12;
(q `1) ^2 <= 1
^2
by A5, A6, SQUARE_1:49;
then A19:
sqrt ((q `1) ^2) <= 1
by A18, SQUARE_1:18, SQUARE_1:26;
|.|[((q `1) / (sqrt (1 + (((q `2) / (q `1)) ^2)))),((q `2) / (sqrt (1 + (((q `2) / (q `1)) ^2))))]|.| ^2 =
(((q `1) / (sqrt (1 + (((q `2) / (q `1)) ^2)))) ^2) + (((q `2) / (sqrt (1 + (((q `2) / (q `1)) ^2)))) ^2)
by A13, A14, JGRAPH_3: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 A15, SQUARE_1:def 2
.=
(((q `1) ^2) / (1 + (((q `2) / (q `1)) ^2))) + (((q `2) ^2) / (1 + (((q `2) / (q `1)) ^2)))
by A15, 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 A18, 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 A16, 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 A19, SQUARE_1:22;
hence
ex
p2 being
Point of
(TOP-REAL 2) st
(
p2 = y &
|.p2.| <= 1 )
by A3, A4, A12;
verum end; case A20:
(
q <> 0. (TOP-REAL 2) & not (
q `2 <= q `1 &
- (q `1) <= q `2 ) & not (
q `2 >= q `1 &
q `2 <= - (q `1) ) )
;
ex p2 being Point of (TOP-REAL 2) st
( p2 = y & |.p2.| <= 1 )then A21:
Sq_Circ . q = |[((q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) / (sqrt (1 + (((q `1) / (q `2)) ^2))))]|
by JGRAPH_3:def 1;
A22:
|[((q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) / (sqrt (1 + (((q `1) / (q `2)) ^2))))]| `1 = (q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))
by EUCLID: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 XREAL_1:34, XREAL_1:63;
A25:
q `2 <> 0
by A20;
then A26:
(q `2) ^2 > 0
by SQUARE_1:12;
(q `2) ^2 <= 1
^2
by A7, A8, SQUARE_1:49;
then A27:
sqrt ((q `2) ^2) <= 1
by A26, SQUARE_1:18, SQUARE_1:26;
|.|[((q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) / (sqrt (1 + (((q `1) / (q `2)) ^2))))]|.| ^2 =
(((q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))) ^2) + (((q `2) / (sqrt (1 + (((q `1) / (q `2)) ^2)))) ^2)
by A22, A23, JGRAPH_3: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 A24, SQUARE_1:def 2
.=
(((q `1) ^2) / (1 + (((q `1) / (q `2)) ^2))) + (((q `2) ^2) / (1 + (((q `1) / (q `2)) ^2)))
by A24, 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 A26, 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 A25, 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 A27, SQUARE_1:22;
hence
ex
p2 being
Point of
(TOP-REAL 2) st
(
p2 = y &
|.p2.| <= 1 )
by A3, A4, A21;
verum end; end; end;
hence
y in Cb
by A1;
verum
end;
let y be object ; TARSKI:def 3 ( not y in Cb or y in Sq_Circ .: Kb )
assume
y in Cb
; y in Sq_Circ .: Kb
then consider p2 being Point of (TOP-REAL 2) such that
A28:
p2 = y
and
A29:
|.p2.| <= 1
by A1;
set q = p2;
now ( ( p2 = 0. (TOP-REAL 2) & ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x ) ) 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 A30:
p2 = 0. (TOP-REAL 2)
;
ex x being set st
( x in dom Sq_Circ & x in Kb & y = Sq_Circ . x )then A31:
p2 `1 = 0
by EUCLID:52, EUCLID:54;
p2 `2 = 0
by A30, EUCLID:52, EUCLID:54;
then A32:
y in Kb
by A1, A28, A31;
A33:
(Sq_Circ ") . y = y
by A28, A30, JGRAPH_3:28;
A34:
dom Sq_Circ = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
y = Sq_Circ . y
by A28, A33, FUNCT_1:35, JGRAPH_3:43;
hence
ex
x being
set st
(
x in dom Sq_Circ &
x in Kb &
y = Sq_Circ . x )
by A32, A34;
verum end; case A35:
(
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 )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 XREAL_1:34, XREAL_1:63;
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 XREAL_1:34, XREAL_1:63;
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 A36, A37, A38, XCMPLX_1:91;
A41:
p2 `1 =
((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by A38, 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
;
A42:
p2 `2 =
((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by A38, 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
;
A43:
|.p2.| ^2 = ((p2 `1) ^2) + ((p2 `2) ^2)
by JGRAPH_3:1;
A44:
|.p2.| ^2 <= 1
^2
by A29, SQUARE_1:15;
A45:
now ( |[((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
;
contradictionA48:
(p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) = 0
by A46, EUCLID:52;
A49:
(p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))) = 0
by A47, EUCLID:52;
A50:
p2 `1 = 0
by A38, A48, XCMPLX_1:6;
p2 `2 = 0
by A38, A49, XCMPLX_1:6;
hence
contradiction
by A35, A50, EUCLID:53, EUCLID:54;
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 A35, A38, XREAL_1:64;
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 A36, A37, A38, 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 A36, A37, A38, XREAL_1:64;
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 A45, JGRAPH_2:3, JGRAPH_3:def 1;
( (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 <= |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 &
- (- (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1)) >= - (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 >= |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 &
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 <= - (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ) )
by A36, A37, A38, A51, XREAL_1:24, XREAL_1:64;
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 A36, A38, A40, XCMPLX_1:89;
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 A37, A38, A40, XCMPLX_1:89;
A56:
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 A36, A37, A38, A45, A51, XREAL_1:64;
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 A40, A41, A42, A43, A44, 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 A39, 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 A39, 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 A39, XREAL_1:64;
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 A39, XCMPLX_1:87;
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 A39, 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 A59, 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 A57, XREAL_1:64;
then
(((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) + (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2) - 1)) * ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) <= (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2
by A57, XCMPLX_1:87;
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))))]| `1) ^2)) + (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) * (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2) - 1))) - ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2) <= 0
by XREAL_1:47;
((((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) * ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2)) + ((((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) * ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2)) - (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) * 1))) - ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2) = (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) - 1) * (((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) + ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2))
;
then
( (
((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) - 1
<= 0 &
((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) - 1
>= 0 ) or (
((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) - 1
<= 0 &
((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) + ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2) >= 0 ) or (
((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) + ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2) <= 0 &
((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) - 1
>= 0 ) or (
((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) + ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2) <= 0 &
((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1) ^2) + ((|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ^2) >= 0 ) )
by A60, XREAL_1:129, XREAL_1:130;
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 A58, XREAL_1:7;
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:47;
A63:
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 >= - (1 ^2)
by A61, SQUARE_1:47;
then
( (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 <= 1 & 1
>= - (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 >= - 1 &
- (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) >= |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `1 ) )
by A53, A62, XXREAL_0:2;
then
( (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 <= 1 &
- 1
<= - (- (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2)) ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 >= - 1 &
- (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2) >= - 1 ) )
by A63, XREAL_1:24, XXREAL_0:2;
then
( (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 <= 1 &
- 1
<= |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2 >= - 1 &
- (- (|[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| `2)) <= - (- 1) ) )
by XREAL_1: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 A28, A52, A54, A55, A56, EUCLID:53;
verum end; case A64:
(
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 )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 A64, JGRAPH_2:13;
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 XREAL_1:34, XREAL_1:63;
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 XREAL_1:34, XREAL_1:63;
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 A66, A67, A68, XCMPLX_1:91;
A71:
p2 `2 =
((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))
by A68, 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
;
A72:
p2 `1 =
((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))
by A68, 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
;
A73:
|.p2.| ^2 = ((p2 `2) ^2) + ((p2 `1) ^2)
by JGRAPH_3:1;
A74:
|.p2.| ^2 <= 1
^2
by A29, SQUARE_1:15;
( (
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 A65, A68, XREAL_1:64;
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 A66, A67, A68, 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 A66, A67, A68, XREAL_1:64;
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 A75, JGRAPH_2:3, JGRAPH_3:4;
( (
|[((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 A66, A67, A68, A79, XREAL_1:24, XREAL_1:64;
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 A66, A68, A70, XCMPLX_1:89;
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 A67, A68, A70, XCMPLX_1:89;
A84:
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 A66, A67, A68, A75, A79, XREAL_1:64;
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 A70, A71, A72, A73, A74, 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 A69, 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 A69, 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 A69, XREAL_1:64;
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 A69, XCMPLX_1:87;
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 A69, 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 A87, 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 A85, XREAL_1:64;
then
(((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) + (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ^2) - 1)) * ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) <= (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ^2
by A85, XCMPLX_1:87;
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))))]| `2) ^2)) + (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2) ^2) * (((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ^2) - 1))) - ((|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ^2) <= 0
by XREAL_1:47;
((((|[((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 A88, XREAL_1:129;
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 A86, XREAL_1:7;
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:47;
A91:
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 >= - (1 ^2)
by A89, SQUARE_1:47;
then
( (
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 <= 1 & 1
>= - (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 >= - 1 &
- (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) >= |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `2 ) )
by A81, A90, XXREAL_0:2;
then
( (
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 <= 1 &
- 1
<= - (- (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1)) ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 >= - 1 &
- (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1) >= - 1 ) )
by A91, XREAL_1:24, XXREAL_0:2;
then
( (
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 <= 1 &
- 1
<= |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 ) or (
|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1 >= - 1 &
- (- (|[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| `1)) <= - (- 1) ) )
by XREAL_1: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 A28, A80, A82, A83, A84, EUCLID:53;
verum end; end; end;
hence
y in Sq_Circ .: Kb
by FUNCT_1:def 6; verum