:: EUCLID_6 semantic presentation

REAL is non empty V35() V126() V127() V128() V132() set
NAT is V126() V127() V128() V129() V130() V131() V132() Element of bool REAL
bool REAL is set
COMPLEX is non empty V35() V126() V132() set
RAT is non empty V35() V126() V127() V128() V129() V132() set
INT is non empty V35() V126() V127() V128() V129() V130() V132() set
[:COMPLEX,COMPLEX:] is complex-valued set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is RAT -valued complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is RAT -valued complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is set
omega is V126() V127() V128() V129() V130() V131() V132() set
bool omega is set
bool NAT is set
K346() is non empty V75() L8()
the carrier of K346() is non empty set
K351() is non empty V75() V97() V98() V99() V101() V148() V149() V150() V151() V152() V153() L8()
K352() is non empty V75() V99() V101() V151() V152() V153() M13(K351())
K353() is non empty V75() V97() V99() V101() V151() V152() V153() V154() M16(K351(),K352())
K355() is non empty V75() V97() V99() V101() L8()
K356() is non empty V75() V97() V99() V101() V154() M13(K355())
[:NAT,REAL:] is complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is set
[:NAT,COMPLEX:] is complex-valued set
bool [:NAT,COMPLEX:] is set
1 is non empty natural complex real ext-real positive non negative V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT
[:1,1:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:1,1:] is set
[:[:1,1:],1:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is set
2 is non empty natural complex real ext-real positive non negative V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT
[:2,2:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
[:[:2,2:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is non empty V73() V138() V139() TopSpace-like V186() V187() V188() V189() V190() V191() V192() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
bool the carrier of (TOP-REAL 2) is set
K559() is non empty strict TopSpace-like V222() TopStruct
the carrier of K559() is non empty V126() V127() V128() set
RealSpace is non empty strict Reflexive discerning V180() triangle Discerning V222() MetrStruct
R^1 is non empty strict TopSpace-like V222() TopStruct
the carrier of R^1 is non empty V126() V127() V128() set
[: the carrier of (TOP-REAL 2), the carrier of R^1:] is complex-valued ext-real-valued real-valued set
bool [: the carrier of (TOP-REAL 2), the carrier of R^1:] is set
{} is empty V126() V127() V128() V129() V130() V131() V132() set
0 is empty natural complex real ext-real non positive non negative V33() V34() V126() V127() V128() V129() V130() V131() V132() Element of NAT
<i> is complex Element of COMPLEX
|.0.| is complex real ext-real Element of REAL
Re 0 is complex real ext-real Element of REAL
(Re 0) ^2 is complex real ext-real Element of REAL
(Re 0) * (Re 0) is complex real ext-real set
Im 0 is complex real ext-real Element of REAL
(Im 0) ^2 is complex real ext-real Element of REAL
(Im 0) * (Im 0) is complex real ext-real set
((Re 0) ^2) + ((Im 0) ^2) is complex real ext-real Element of REAL
sqrt (((Re 0) ^2) + ((Im 0) ^2)) is complex real ext-real Element of REAL
PI is non empty complex real ext-real positive non negative Element of REAL
2 * PI is non empty complex real ext-real positive non negative Element of REAL
5 is non empty natural complex real ext-real positive non negative V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT
5 * PI is non empty complex real ext-real positive non negative Element of REAL
PI / 2 is non empty complex real ext-real positive non negative Element of REAL
3 is non empty natural complex real ext-real positive non negative V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT
3 / 2 is non empty complex real ext-real positive non negative Element of REAL
(3 / 2) * PI is non empty complex real ext-real positive non negative Element of REAL
0. (TOP-REAL 2) is Relation-like Function-like V42(2) FinSequence-like zero complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
euc2cpx (0. (TOP-REAL 2)) is complex Element of COMPLEX
(0. (TOP-REAL 2)) `1 is complex real ext-real Element of REAL
K367((0. (TOP-REAL 2)),1) is complex real ext-real Element of REAL
(0. (TOP-REAL 2)) `2 is complex real ext-real Element of REAL
K367((0. (TOP-REAL 2)),2) is complex real ext-real Element of REAL
((0. (TOP-REAL 2)) `2) * <i> is complex set
((0. (TOP-REAL 2)) `1) + (((0. (TOP-REAL 2)) `2) * <i>) is complex set
0c is empty complex V126() V127() V128() V129() V130() V131() V132() Element of COMPLEX
cos is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
sin is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K535(REAL,sin) is V126() V127() V128() Element of bool REAL
K535(REAL,cos) is V126() V127() V128() Element of bool REAL
K367(cos,0) is complex real ext-real Element of REAL
K367(sin,0) is complex real ext-real Element of REAL
cos 0 is complex real ext-real Element of REAL
sin 0 is complex real ext-real Element of REAL
cos (PI / 2) is complex real ext-real Element of REAL
sin (PI / 2) is complex real ext-real Element of REAL
cos PI is complex real ext-real Element of REAL
- 1 is non empty complex real ext-real non positive negative Element of REAL
sin PI is complex real ext-real Element of REAL
PI + (PI / 2) is non empty complex real ext-real positive non negative Element of REAL
cos (PI + (PI / 2)) is complex real ext-real Element of REAL
sin (PI + (PI / 2)) is complex real ext-real Element of REAL
cos (2 * PI) is complex real ext-real Element of REAL
sin (2 * PI) is complex real ext-real Element of REAL
ExtREAL is non empty V127() set
I[01] is non empty strict TopSpace-like V222() SubSpace of R^1
the carrier of I[01] is non empty V126() V127() V128() set
[.0,1.] is V126() V127() V128() Element of bool REAL
TopSpaceMetr RealSpace is TopStruct
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V222() SubSpace of R^1
real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p1 - p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- 1 is non empty complex real ext-real non positive negative set
(- 1) * p2 is Relation-like Function-like set
K214((TOP-REAL 2),p1,(- p2)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] -defined the carrier of (TOP-REAL 2) -valued Function-like total V30([: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2)) Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]
[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is set
[:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is set
bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is set
K414( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p1,(- p2)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p1 + (- p2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
p1 - p2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K280(p2) is Relation-like Function-like complex-valued set
K251(p1,K280(p2)) is Relation-like Function-like set
|.(p1 - p2).| is complex real ext-real non negative Element of REAL
sqr (p1 - p2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((p1 - p2),(p1 - p2)) is Relation-like Function-like set
K339((sqr (p1 - p2))) is complex real ext-real Element of REAL
sqrt K339((sqr (p1 - p2))) is complex real ext-real Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p1 - p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- 1 is non empty complex real ext-real non positive negative set
(- 1) * p2 is Relation-like Function-like set
K214((TOP-REAL 2),p1,(- p2)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] -defined the carrier of (TOP-REAL 2) -valued Function-like total V30([: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2)) Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]
[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is set
[:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is set
bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is set
K414( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p1,(- p2)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p1 + (- p2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
p1 - p2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K280(p2) is Relation-like Function-like complex-valued set
K251(p1,K280(p2)) is Relation-like Function-like set
|.(p1 - p2).| is complex real ext-real non negative Element of REAL
sqr (p1 - p2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((p1 - p2),(p1 - p2)) is Relation-like Function-like set
K339((sqr (p1 - p2))) is complex real ext-real Element of REAL
sqrt K339((sqr (p1 - p2))) is complex real ext-real Element of REAL
p2 - p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
- p1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- 1) * p1 is Relation-like Function-like set
K214((TOP-REAL 2),p2,(- p1)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
K414( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p2,(- p1)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 + (- p1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
p2 - p1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K280(p1) is Relation-like Function-like complex-valued set
K251(p2,K280(p1)) is Relation-like Function-like set
|.(p2 - p1).| is complex real ext-real non negative Element of REAL
sqr (p2 - p1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((p2 - p1),(p2 - p1)) is Relation-like Function-like set
K339((sqr (p2 - p1))) is complex real ext-real Element of REAL
sqrt K339((sqr (p2 - p1))) is complex real ext-real Element of REAL
REAL 2 is non empty FinSequence-membered M10( REAL )
K318(2,REAL) is FinSequence-membered M10( REAL )
p3 is Relation-like NAT -defined REAL -valued Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 2
|.p3.| is complex real ext-real non negative Element of REAL
sqr p3 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt (p3,p3) is Relation-like Function-like set
K339((sqr p3)) is complex real ext-real Element of REAL
sqrt K339((sqr p3)) is complex real ext-real Element of REAL
- p3 is Relation-like NAT -defined REAL -valued Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of REAL 2
(- 1) * p3 is Relation-like Function-like set
|.(- p3).| is complex real ext-real non negative Element of REAL
sqr (- p3) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((- p3),(- p3)) is Relation-like Function-like set
K339((sqr (- p3))) is complex real ext-real Element of REAL
sqrt K339((sqr (- p3))) is complex real ext-real Element of REAL
- (p1 - p2) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
- (p1 - p2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- 1) * (p1 - p2) is Relation-like Function-like set
|.(- (p1 - p2)).| is complex real ext-real non negative Element of REAL
sqr (- (p1 - p2)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((- (p1 - p2)),(- (p1 - p2))) is Relation-like Function-like set
K339((sqr (- (p1 - p2)))) is complex real ext-real Element of REAL
sqrt K339((sqr (- (p1 - p2)))) is complex real ext-real Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p1,p2,p3) is complex real ext-real Element of REAL
euc2cpx p1 is complex Element of COMPLEX
p1 `1 is complex real ext-real Element of REAL
K367(p1,1) is complex real ext-real Element of REAL
p1 `2 is complex real ext-real Element of REAL
K367(p1,2) is complex real ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
euc2cpx p2 is complex Element of COMPLEX
p2 `1 is complex real ext-real Element of REAL
K367(p2,1) is complex real ext-real Element of REAL
p2 `2 is complex real ext-real Element of REAL
K367(p2,2) is complex real ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
euc2cpx p3 is complex Element of COMPLEX
p3 `1 is complex real ext-real Element of REAL
K367(p3,1) is complex real ext-real Element of REAL
p3 `2 is complex real ext-real Element of REAL
K367(p3,2) is complex real ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is complex real ext-real set
sin (angle (p1,p2,p3)) is complex real ext-real Element of REAL
cos (angle (p1,p2,p3)) is complex real ext-real Element of REAL
p4 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
a is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p4,p,a) is complex real ext-real Element of REAL
euc2cpx p4 is complex Element of COMPLEX
p4 `1 is complex real ext-real Element of REAL
K367(p4,1) is complex real ext-real Element of REAL
p4 `2 is complex real ext-real Element of REAL
K367(p4,2) is complex real ext-real Element of REAL
(p4 `2) * <i> is complex set
(p4 `1) + ((p4 `2) * <i>) is complex set
euc2cpx p is complex Element of COMPLEX
p `1 is complex real ext-real Element of REAL
K367(p,1) is complex real ext-real Element of REAL
p `2 is complex real ext-real Element of REAL
K367(p,2) is complex real ext-real Element of REAL
(p `2) * <i> is complex set
(p `1) + ((p `2) * <i>) is complex set
euc2cpx a is complex Element of COMPLEX
a `1 is complex real ext-real Element of REAL
K367(a,1) is complex real ext-real Element of REAL
a `2 is complex real ext-real Element of REAL
K367(a,2) is complex real ext-real Element of REAL
(a `2) * <i> is complex set
(a `1) + ((a `2) * <i>) is complex set
angle ((euc2cpx p4),(euc2cpx p),(euc2cpx a)) is complex real ext-real set
sin (angle (p4,p,a)) is complex real ext-real Element of REAL
cos (angle (p4,p,a)) is complex real ext-real Element of REAL
(2 * PI) * 0 is empty complex real ext-real non positive non negative V126() V127() V128() V129() V130() V131() V132() Element of REAL
(2 * PI) + ((2 * PI) * 0) is non empty complex real ext-real positive non negative Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p1,p2,p3) is complex real ext-real Element of REAL
euc2cpx p1 is complex Element of COMPLEX
p1 `1 is complex real ext-real Element of REAL
K367(p1,1) is complex real ext-real Element of REAL
p1 `2 is complex real ext-real Element of REAL
K367(p1,2) is complex real ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
euc2cpx p2 is complex Element of COMPLEX
p2 `1 is complex real ext-real Element of REAL
K367(p2,1) is complex real ext-real Element of REAL
p2 `2 is complex real ext-real Element of REAL
K367(p2,2) is complex real ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
euc2cpx p3 is complex Element of COMPLEX
p3 `1 is complex real ext-real Element of REAL
K367(p3,1) is complex real ext-real Element of REAL
p3 `2 is complex real ext-real Element of REAL
K367(p3,2) is complex real ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is complex real ext-real set
sin (angle (p1,p2,p3)) is complex real ext-real Element of REAL
angle (p3,p2,p1) is complex real ext-real Element of REAL
angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) is complex real ext-real set
sin (angle (p3,p2,p1)) is complex real ext-real Element of REAL
- (sin (angle (p3,p2,p1))) is complex real ext-real Element of REAL
(2 * PI) - (angle (p1,p2,p3)) is complex real ext-real Element of REAL
- (angle (p3,p2,p1)) is complex real ext-real Element of REAL
(- (angle (p3,p2,p1))) + (2 * PI) is complex real ext-real Element of REAL
sin ((- (angle (p3,p2,p1))) + (2 * PI)) is complex real ext-real Element of REAL
sin (- (angle (p3,p2,p1))) is complex real ext-real Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p1,p2,p3) is complex real ext-real Element of REAL
euc2cpx p1 is complex Element of COMPLEX
p1 `1 is complex real ext-real Element of REAL
K367(p1,1) is complex real ext-real Element of REAL
p1 `2 is complex real ext-real Element of REAL
K367(p1,2) is complex real ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
euc2cpx p2 is complex Element of COMPLEX
p2 `1 is complex real ext-real Element of REAL
K367(p2,1) is complex real ext-real Element of REAL
p2 `2 is complex real ext-real Element of REAL
K367(p2,2) is complex real ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
euc2cpx p3 is complex Element of COMPLEX
p3 `1 is complex real ext-real Element of REAL
K367(p3,1) is complex real ext-real Element of REAL
p3 `2 is complex real ext-real Element of REAL
K367(p3,2) is complex real ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is complex real ext-real set
cos (angle (p1,p2,p3)) is complex real ext-real Element of REAL
angle (p3,p2,p1) is complex real ext-real Element of REAL
angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) is complex real ext-real set
cos (angle (p3,p2,p1)) is complex real ext-real Element of REAL
(2 * PI) - (angle (p1,p2,p3)) is complex real ext-real Element of REAL
- (angle (p3,p2,p1)) is complex real ext-real Element of REAL
(- (angle (p3,p2,p1))) + (2 * PI) is complex real ext-real Element of REAL
cos ((- (angle (p3,p2,p1))) + (2 * PI)) is complex real ext-real Element of REAL
cos (- (angle (p3,p2,p1))) is complex real ext-real Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p1,p2,p3) is complex real ext-real Element of REAL
euc2cpx p1 is complex Element of COMPLEX
p1 `1 is complex real ext-real Element of REAL
K367(p1,1) is complex real ext-real Element of REAL
p1 `2 is complex real ext-real Element of REAL
K367(p1,2) is complex real ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
euc2cpx p2 is complex Element of COMPLEX
p2 `1 is complex real ext-real Element of REAL
K367(p2,1) is complex real ext-real Element of REAL
p2 `2 is complex real ext-real Element of REAL
K367(p2,2) is complex real ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
euc2cpx p3 is complex Element of COMPLEX
p3 `1 is complex real ext-real Element of REAL
K367(p3,1) is complex real ext-real Element of REAL
p3 `2 is complex real ext-real Element of REAL
K367(p3,2) is complex real ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is complex real ext-real set
p4 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
a is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p4,p,a) is complex real ext-real Element of REAL
euc2cpx p4 is complex Element of COMPLEX
p4 `1 is complex real ext-real Element of REAL
K367(p4,1) is complex real ext-real Element of REAL
p4 `2 is complex real ext-real Element of REAL
K367(p4,2) is complex real ext-real Element of REAL
(p4 `2) * <i> is complex set
(p4 `1) + ((p4 `2) * <i>) is complex set
euc2cpx p is complex Element of COMPLEX
p `1 is complex real ext-real Element of REAL
K367(p,1) is complex real ext-real Element of REAL
p `2 is complex real ext-real Element of REAL
K367(p,2) is complex real ext-real Element of REAL
(p `2) * <i> is complex set
(p `1) + ((p `2) * <i>) is complex set
euc2cpx a is complex Element of COMPLEX
a `1 is complex real ext-real Element of REAL
K367(a,1) is complex real ext-real Element of REAL
a `2 is complex real ext-real Element of REAL
K367(a,2) is complex real ext-real Element of REAL
(a `2) * <i> is complex set
(a `1) + ((a `2) * <i>) is complex set
angle ((euc2cpx p4),(euc2cpx p),(euc2cpx a)) is complex real ext-real set
2 * (angle (p4,p,a)) is complex real ext-real Element of REAL
(2 * (angle (p4,p,a))) + (2 * PI) is complex real ext-real Element of REAL
0 + (2 * PI) is non empty complex real ext-real positive non negative Element of REAL
(angle (p4,p,a)) * 2 is complex real ext-real Element of REAL
((angle (p4,p,a)) * 2) + (2 * PI) is complex real ext-real Element of REAL
4 is non empty natural complex real ext-real positive non negative V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT
4 * PI is non empty complex real ext-real positive non negative Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p1,p2,p3) is complex real ext-real Element of REAL
euc2cpx p1 is complex Element of COMPLEX
p1 `1 is complex real ext-real Element of REAL
K367(p1,1) is complex real ext-real Element of REAL
p1 `2 is complex real ext-real Element of REAL
K367(p1,2) is complex real ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
euc2cpx p2 is complex Element of COMPLEX
p2 `1 is complex real ext-real Element of REAL
K367(p2,1) is complex real ext-real Element of REAL
p2 `2 is complex real ext-real Element of REAL
K367(p2,2) is complex real ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
euc2cpx p3 is complex Element of COMPLEX
p3 `1 is complex real ext-real Element of REAL
K367(p3,1) is complex real ext-real Element of REAL
p3 `2 is complex real ext-real Element of REAL
K367(p3,2) is complex real ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is complex real ext-real set
p4 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
a is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p4,p,a) is complex real ext-real Element of REAL
euc2cpx p4 is complex Element of COMPLEX
p4 `1 is complex real ext-real Element of REAL
K367(p4,1) is complex real ext-real Element of REAL
p4 `2 is complex real ext-real Element of REAL
K367(p4,2) is complex real ext-real Element of REAL
(p4 `2) * <i> is complex set
(p4 `1) + ((p4 `2) * <i>) is complex set
euc2cpx p is complex Element of COMPLEX
p `1 is complex real ext-real Element of REAL
K367(p,1) is complex real ext-real Element of REAL
p `2 is complex real ext-real Element of REAL
K367(p,2) is complex real ext-real Element of REAL
(p `2) * <i> is complex set
(p `1) + ((p `2) * <i>) is complex set
euc2cpx a is complex Element of COMPLEX
a `1 is complex real ext-real Element of REAL
K367(a,1) is complex real ext-real Element of REAL
a `2 is complex real ext-real Element of REAL
K367(a,2) is complex real ext-real Element of REAL
(a `2) * <i> is complex set
(a `1) + ((a `2) * <i>) is complex set
angle ((euc2cpx p4),(euc2cpx p),(euc2cpx a)) is complex real ext-real set
2 * (angle (p4,p,a)) is complex real ext-real Element of REAL
(2 * (angle (p4,p,a))) + (4 * PI) is complex real ext-real Element of REAL
0 + (4 * PI) is non empty complex real ext-real positive non negative Element of REAL
(angle (p4,p,a)) * 2 is complex real ext-real Element of REAL
((angle (p4,p,a)) * 2) + (4 * PI) is complex real ext-real Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p1,p2,p3) is complex real ext-real Element of REAL
euc2cpx p1 is complex Element of COMPLEX
p1 `1 is complex real ext-real Element of REAL
K367(p1,1) is complex real ext-real Element of REAL
p1 `2 is complex real ext-real Element of REAL
K367(p1,2) is complex real ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
euc2cpx p2 is complex Element of COMPLEX
p2 `1 is complex real ext-real Element of REAL
K367(p2,1) is complex real ext-real Element of REAL
p2 `2 is complex real ext-real Element of REAL
K367(p2,2) is complex real ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
euc2cpx p3 is complex Element of COMPLEX
p3 `1 is complex real ext-real Element of REAL
K367(p3,1) is complex real ext-real Element of REAL
p3 `2 is complex real ext-real Element of REAL
K367(p3,2) is complex real ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is complex real ext-real set
p4 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
a is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p4,p,a) is complex real ext-real Element of REAL
euc2cpx p4 is complex Element of COMPLEX
p4 `1 is complex real ext-real Element of REAL
K367(p4,1) is complex real ext-real Element of REAL
p4 `2 is complex real ext-real Element of REAL
K367(p4,2) is complex real ext-real Element of REAL
(p4 `2) * <i> is complex set
(p4 `1) + ((p4 `2) * <i>) is complex set
euc2cpx p is complex Element of COMPLEX
p `1 is complex real ext-real Element of REAL
K367(p,1) is complex real ext-real Element of REAL
p `2 is complex real ext-real Element of REAL
K367(p,2) is complex real ext-real Element of REAL
(p `2) * <i> is complex set
(p `1) + ((p `2) * <i>) is complex set
euc2cpx a is complex Element of COMPLEX
a `1 is complex real ext-real Element of REAL
K367(a,1) is complex real ext-real Element of REAL
a `2 is complex real ext-real Element of REAL
K367(a,2) is complex real ext-real Element of REAL
(a `2) * <i> is complex set
(a `1) + ((a `2) * <i>) is complex set
angle ((euc2cpx p4),(euc2cpx p),(euc2cpx a)) is complex real ext-real set
2 * (angle (p4,p,a)) is complex real ext-real Element of REAL
(2 * (angle (p4,p,a))) - (4 * PI) is complex real ext-real Element of REAL
(2 * PI) * 2 is non empty complex real ext-real positive non negative Element of REAL
(angle (p4,p,a)) * 2 is complex real ext-real Element of REAL
(4 * PI) - (4 * PI) is complex real ext-real Element of REAL
((angle (p4,p,a)) * 2) - (4 * PI) is complex real ext-real Element of REAL
6 is non empty natural complex real ext-real positive non negative V33() V34() V126() V127() V128() V129() V130() V131() Element of NAT
6 * PI is non empty complex real ext-real positive non negative Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p3 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p1,p2,p3) is complex real ext-real Element of REAL
euc2cpx p1 is complex Element of COMPLEX
p1 `1 is complex real ext-real Element of REAL
K367(p1,1) is complex real ext-real Element of REAL
p1 `2 is complex real ext-real Element of REAL
K367(p1,2) is complex real ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
euc2cpx p2 is complex Element of COMPLEX
p2 `1 is complex real ext-real Element of REAL
K367(p2,1) is complex real ext-real Element of REAL
p2 `2 is complex real ext-real Element of REAL
K367(p2,2) is complex real ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
euc2cpx p3 is complex Element of COMPLEX
p3 `1 is complex real ext-real Element of REAL
K367(p3,1) is complex real ext-real Element of REAL
p3 `2 is complex real ext-real Element of REAL
K367(p3,2) is complex real ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is complex real ext-real set
p4 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
a is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
angle (p4,p,a) is complex real ext-real Element of REAL
euc2cpx p4 is complex Element of COMPLEX
p4 `1 is complex real ext-real Element of REAL
K367(p4,1) is complex real ext-real Element of REAL
p4 `2 is complex real ext-real Element of REAL
K367(p4,2) is complex real ext-real Element of REAL
(p4 `2) * <i> is complex set
(p4 `1) + ((p4 `2) * <i>) is complex set
euc2cpx p is complex Element of COMPLEX
p `1 is complex real ext-real Element of REAL
K367(p,1) is complex real ext-real Element of REAL
p `2 is complex real ext-real Element of REAL
K367(p,2) is complex real ext-real Element of REAL
(p `2) * <i> is complex set
(p `1) + ((p `2) * <i>) is complex set
euc2cpx a is complex Element of COMPLEX
a `1 is complex real ext-real Element of REAL
K367(a,1) is complex real ext-real Element of REAL
a `2 is complex real ext-real Element of REAL
K367(a,2) is complex real ext-real Element of REAL
(a `2) * <i> is complex set
(a `1) + ((a `2) * <i>) is complex set
angle ((euc2cpx p4),(euc2cpx p),(euc2cpx a)) is complex real ext-real set
2 * (angle (p4,p,a)) is complex real ext-real Element of REAL
(2 * (angle (p4,p,a))) - (6 * PI) is complex real ext-real Element of REAL
(2 * PI) * 2 is non empty complex real ext-real positive non negative Element of REAL
(angle (p4,p,a)) * 2 is complex real ext-real Element of REAL
- 2 is non empty complex real ext-real non positive negative Element of REAL
PI * (- 2) is non empty complex real ext-real non positive negative Element of REAL
0 * (- 2) is empty complex real ext-real non positive non negative V126() V127() V128() V129() V130() V131() V132() Element of REAL
(4 * PI) - (6 * PI) is complex real ext-real Element of REAL
((angle (p4,p,a)) * 2) - (6 * PI) is complex real ext-real Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p1 - p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
- p2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- 1 is non empty complex real ext-real non positive negative set
(- 1) * p2 is Relation-like Function-like set
K214((TOP-REAL 2),p1,(- p2)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
the U5 of (TOP-REAL 2) is Relation-like [: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] -defined the carrier of (TOP-REAL 2) -valued Function-like total V30([: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2)) Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]
[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is set
[:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is set
bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is set
K414( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p1,(- p2)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p1 + (- p2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
p1 - p2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K280(p2) is Relation-like Function-like complex-valued set
K251(p1,K280(p2)) is Relation-like Function-like set
euc2cpx (p1 - p2) is complex Element of COMPLEX
(p1 - p2) `1 is complex real ext-real Element of REAL
K367((p1 - p2),1) is complex real ext-real Element of REAL
(p1 - p2) `2 is complex real ext-real Element of REAL
K367((p1 - p2),2) is complex real ext-real Element of REAL
((p1 - p2) `2) * <i> is complex set
((p1 - p2) `1) + (((p1 - p2) `2) * <i>) is complex set
p3 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p3 - p2 is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
K214((TOP-REAL 2),p3,(- p2)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
K414( the carrier of (TOP-REAL 2), the U5 of (TOP-REAL 2),p3,(- p2)) is Relation-like Function-like V42(2) FinSequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL 2)
p3 + (- p2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
p3 - p2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K251(p3,K280(p2)) is Relation-like Function-like set
euc2cpx (p3 - p2) is complex Element of COMPLEX
(p3 - p2) `1 is complex real ext-real Element of REAL
K367((p3 - p2),1) is complex real ext-real Element of REAL
(p3 - p2) `2 is complex real ext-real Element of REAL
K367((p3 - p2),2) is complex real ext-real Element of REAL
((p3 - p2) `2) * <i> is complex set
((p3 - p2) `1) + (((p3 - p2) `2) * <i>) is complex set
angle (p1,p2,p3) is complex real ext-real Element of REAL
euc2cpx p1 is complex Element of COMPLEX
p1 `1 is complex real ext-real Element of REAL
K367(p1,1) is complex real ext-real Element of REAL
p1 `2 is complex real ext-real Element of REAL
K367(p1,2) is complex real ext-real Element of REAL
(p1 `2) * <i> is complex set
(p1 `1) + ((p1 `2) * <i>) is complex set
euc2cpx p2 is complex Element of COMPLEX
p2 `1 is complex real ext-real Element of REAL
K367(p2,1) is complex real ext-real Element of REAL
p2 `2 is complex real ext-real Element of REAL
K367(p2,2) is complex real ext-real Element of REAL
(p2 `2) * <i> is complex set
(p2 `1) + ((p2 `2) * <i>) is complex set
euc2cpx p3 is complex Element of COMPLEX
p3 `1 is complex real ext-real Element of REAL
K367(p3,1) is complex real ext-real Element of REAL
p3 `2 is complex real ext-real Element of REAL
K367(p3,2) is complex real ext-real Element of REAL
(p3 `2) * <i> is complex set
(p3 `1) + ((p3 `2) * <i>) is complex set
angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is complex real ext-real set
p4 is complex Element of COMPLEX
p is complex Element of COMPLEX
angle (p4,p) is complex real ext-real Element of REAL
angle ((p1 - p2),(0. (TOP-REAL 2)),(p3 - p2)) is complex real ext-real Element of REAL
angle ((euc2cpx (p1 - p2)),(euc2cpx (0. (TOP-REAL 2))),(euc2cpx (p3 - p2))) is complex real ext-real set
p2 is complex Element of COMPLEX
p1 is complex Element of COMPLEX
Arg p1 is complex real ext-real Element of REAL
- (Arg p1) is complex real ext-real Element of REAL
Rotate (p2,(- (Arg p1))) is complex Element of COMPLEX
Arg (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
p2 is complex Element of COMPLEX
p1 is complex Element of COMPLEX
Arg p1 is complex real ext-real Element of REAL
angle (p1,p2) is complex real ext-real Element of REAL
- (Arg p1) is complex real ext-real Element of REAL
Rotate (p2,(- (Arg p1))) is complex Element of COMPLEX
Arg (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
p2 is complex Element of COMPLEX
Arg p2 is complex real ext-real Element of REAL
p1 is complex Element of COMPLEX
Arg p1 is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
- (Arg p1) is complex real ext-real Element of REAL
Rotate (p2,(- (Arg p1))) is complex Element of COMPLEX
Arg (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
(- (Arg p1)) + (Arg p2) is complex real ext-real Element of REAL
(2 * PI) + (Arg p1) is complex real ext-real Element of REAL
(Arg p2) + 0 is complex real ext-real Element of REAL
|.p2.| is complex real ext-real Element of REAL
Re p2 is complex real ext-real Element of REAL
(Re p2) ^2 is complex real ext-real Element of REAL
(Re p2) * (Re p2) is complex real ext-real set
Im p2 is complex real ext-real Element of REAL
(Im p2) ^2 is complex real ext-real Element of REAL
(Im p2) * (Im p2) is complex real ext-real set
((Re p2) ^2) + ((Im p2) ^2) is complex real ext-real Element of REAL
sqrt (((Re p2) ^2) + ((Im p2) ^2)) is complex real ext-real Element of REAL
cos ((- (Arg p1)) + (Arg p2)) is complex real ext-real Element of REAL
|.p2.| * (cos ((- (Arg p1)) + (Arg p2))) is complex real ext-real Element of REAL
sin ((- (Arg p1)) + (Arg p2)) is complex real ext-real Element of REAL
|.p2.| * (sin ((- (Arg p1)) + (Arg p2))) is complex real ext-real Element of REAL
(|.p2.| * (sin ((- (Arg p1)) + (Arg p2)))) * <i> is complex set
(|.p2.| * (cos ((- (Arg p1)) + (Arg p2)))) + ((|.p2.| * (sin ((- (Arg p1)) + (Arg p2)))) * <i>) is complex set
((2 * PI) + (Arg p1)) - (Arg p1) is complex real ext-real Element of REAL
|.(Rotate (p2,(- (Arg p1)))).| is complex real ext-real Element of REAL
Re (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
(Re (Rotate (p2,(- (Arg p1))))) ^2 is complex real ext-real Element of REAL
(Re (Rotate (p2,(- (Arg p1))))) * (Re (Rotate (p2,(- (Arg p1))))) is complex real ext-real set
Im (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
(Im (Rotate (p2,(- (Arg p1))))) ^2 is complex real ext-real Element of REAL
(Im (Rotate (p2,(- (Arg p1))))) * (Im (Rotate (p2,(- (Arg p1))))) is complex real ext-real set
((Re (Rotate (p2,(- (Arg p1))))) ^2) + ((Im (Rotate (p2,(- (Arg p1))))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Rotate (p2,(- (Arg p1))))) ^2) + ((Im (Rotate (p2,(- (Arg p1))))) ^2)) is complex real ext-real Element of REAL
p2 is complex Element of COMPLEX
Arg p2 is complex real ext-real Element of REAL
p1 is complex Element of COMPLEX
Arg p1 is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
angle (p1,p2) is complex real ext-real Element of REAL
- (Arg p1) is complex real ext-real Element of REAL
Rotate (p2,(- (Arg p1))) is complex Element of COMPLEX
Arg (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
p2 is complex Element of COMPLEX
Arg p2 is complex real ext-real Element of REAL
p1 is complex Element of COMPLEX
Arg p1 is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
- (Arg p1) is complex real ext-real Element of REAL
Rotate (p2,(- (Arg p1))) is complex Element of COMPLEX
Arg (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (Arg p2) is complex real ext-real Element of REAL
(- (Arg p1)) + (Arg p2) is complex real ext-real Element of REAL
0 + (2 * PI) is non empty complex real ext-real positive non negative Element of REAL
((- (Arg p1)) + (Arg p2)) + (2 * PI) is complex real ext-real Element of REAL
|.p2.| is complex real ext-real Element of REAL
Re p2 is complex real ext-real Element of REAL
(Re p2) ^2 is complex real ext-real Element of REAL
(Re p2) * (Re p2) is complex real ext-real set
Im p2 is complex real ext-real Element of REAL
(Im p2) ^2 is complex real ext-real Element of REAL
(Im p2) * (Im p2) is complex real ext-real set
((Re p2) ^2) + ((Im p2) ^2) is complex real ext-real Element of REAL
sqrt (((Re p2) ^2) + ((Im p2) ^2)) is complex real ext-real Element of REAL
cos ((- (Arg p1)) + (Arg p2)) is complex real ext-real Element of REAL
|.p2.| * (cos ((- (Arg p1)) + (Arg p2))) is complex real ext-real Element of REAL
sin ((- (Arg p1)) + (Arg p2)) is complex real ext-real Element of REAL
|.p2.| * (sin ((- (Arg p1)) + (Arg p2))) is complex real ext-real Element of REAL
(|.p2.| * (sin ((- (Arg p1)) + (Arg p2)))) * <i> is complex set
(|.p2.| * (cos ((- (Arg p1)) + (Arg p2)))) + ((|.p2.| * (sin ((- (Arg p1)) + (Arg p2)))) * <i>) is complex set
(2 * PI) * 1 is non empty complex real ext-real positive non negative Element of REAL
((2 * PI) * 1) + ((- (Arg p1)) + (Arg p2)) is complex real ext-real Element of REAL
cos (((2 * PI) * 1) + ((- (Arg p1)) + (Arg p2))) is complex real ext-real Element of REAL
|.p2.| * (cos (((2 * PI) * 1) + ((- (Arg p1)) + (Arg p2)))) is complex real ext-real Element of REAL
(|.p2.| * (cos (((2 * PI) * 1) + ((- (Arg p1)) + (Arg p2))))) + ((|.p2.| * (sin ((- (Arg p1)) + (Arg p2)))) * <i>) is complex set
(2 * PI) + ((- (Arg p1)) + (Arg p2)) is complex real ext-real Element of REAL
cos ((2 * PI) + ((- (Arg p1)) + (Arg p2))) is complex real ext-real Element of REAL
|.p2.| * (cos ((2 * PI) + ((- (Arg p1)) + (Arg p2)))) is complex real ext-real Element of REAL
sin (((2 * PI) * 1) + ((- (Arg p1)) + (Arg p2))) is complex real ext-real Element of REAL
|.p2.| * (sin (((2 * PI) * 1) + ((- (Arg p1)) + (Arg p2)))) is complex real ext-real Element of REAL
(|.p2.| * (sin (((2 * PI) * 1) + ((- (Arg p1)) + (Arg p2))))) * <i> is complex set
(|.p2.| * (cos ((2 * PI) + ((- (Arg p1)) + (Arg p2))))) + ((|.p2.| * (sin (((2 * PI) * 1) + ((- (Arg p1)) + (Arg p2))))) * <i>) is complex set
(Arg p1) + 0 is complex real ext-real Element of REAL
(2 * PI) + (Arg p2) is complex real ext-real Element of REAL
(Arg p1) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) + (Arg p2)) - (Arg p1) is complex real ext-real Element of REAL
|.(Rotate (p2,(- (Arg p1)))).| is complex real ext-real Element of REAL
Re (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
(Re (Rotate (p2,(- (Arg p1))))) ^2 is complex real ext-real Element of REAL
(Re (Rotate (p2,(- (Arg p1))))) * (Re (Rotate (p2,(- (Arg p1))))) is complex real ext-real set
Im (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
(Im (Rotate (p2,(- (Arg p1))))) ^2 is complex real ext-real Element of REAL
(Im (Rotate (p2,(- (Arg p1))))) * (Im (Rotate (p2,(- (Arg p1))))) is complex real ext-real set
((Re (Rotate (p2,(- (Arg p1))))) ^2) + ((Im (Rotate (p2,(- (Arg p1))))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Rotate (p2,(- (Arg p1))))) ^2) + ((Im (Rotate (p2,(- (Arg p1))))) ^2)) is complex real ext-real Element of REAL
p2 is complex Element of COMPLEX
Arg p2 is complex real ext-real Element of REAL
p1 is complex Element of COMPLEX
Arg p1 is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
angle (p1,p2) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (Arg p2) is complex real ext-real Element of REAL
- (Arg p1) is complex real ext-real Element of REAL
Rotate (p2,(- (Arg p1))) is complex Element of COMPLEX
Arg (Rotate (p2,(- (Arg p1)))) is complex real ext-real Element of REAL
p1 is complex Element of COMPLEX
p2 is complex Element of COMPLEX
angle (p1,p2) is complex real ext-real Element of REAL
p3 is complex Element of COMPLEX
angle (p2,p3) is complex real ext-real Element of REAL
(angle (p1,p2)) + (angle (p2,p3)) is complex real ext-real Element of REAL
angle (p1,p3) is complex real ext-real Element of REAL
(angle (p1,p3)) + (2 * PI) is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
0 + (angle (p2,p3)) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (angle (p2,p3)) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + 0 is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
((Arg p2) - (Arg p1)) + (angle (p2,p3)) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (Arg p2) is complex real ext-real Element of REAL
(((2 * PI) - (Arg p1)) + (Arg p2)) + (angle (p2,p3)) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
- (Arg p1) is complex real ext-real Element of REAL
- (- (Arg p1)) is complex real ext-real Element of REAL
- 0 is empty complex real ext-real non positive non negative V126() V127() V128() V129() V130() V131() V132() Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
((Arg p2) - (Arg p1)) + (angle (p2,p3)) is complex real ext-real Element of REAL
(2 * PI) - (Arg p2) is complex real ext-real Element of REAL
(Arg p2) + ((2 * PI) - (Arg p2)) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (Arg p2) is complex real ext-real Element of REAL
(((2 * PI) - (Arg p1)) + (Arg p2)) + (angle (p2,p3)) is complex real ext-real Element of REAL
(2 * PI) - (Arg p2) is complex real ext-real Element of REAL
(((2 * PI) - (Arg p1)) + (Arg p2)) + ((2 * PI) - (Arg p2)) is complex real ext-real Element of REAL
(2 * PI) + (2 * PI) is non empty complex real ext-real positive non negative Element of REAL
((2 * PI) + (2 * PI)) - (Arg p1) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((Arg p2) - (Arg p1)) + (angle (p2,p3)) is complex real ext-real Element of REAL
(2 * PI) - (Arg p2) is complex real ext-real Element of REAL
((Arg p2) - (Arg p1)) + ((2 * PI) - (Arg p2)) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
Arg p3 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p3) - (Arg p2) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
(Arg p3) - (Arg p1) is complex real ext-real Element of REAL
(Arg p3) - 0 is complex real ext-real Element of REAL
Arg p3 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p3) - (Arg p2) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
(Arg p3) - (Arg p1) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (angle (p2,p3)) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + ((Arg p3) - (Arg p2)) is complex real ext-real Element of REAL
(Arg p3) - 0 is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + ((Arg p3) - 0) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (Arg p3) is complex real ext-real Element of REAL
Arg p3 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p3) - (Arg p2) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
(Arg p3) - (Arg p1) is complex real ext-real Element of REAL
(Arg p3) - 0 is complex real ext-real Element of REAL
Arg p3 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p3) - (Arg p2) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
(Arg p3) - (Arg p1) is complex real ext-real Element of REAL
0 + (angle (p2,p3)) is complex real ext-real Element of REAL
0 + ((Arg p3) - (Arg p2)) is complex real ext-real Element of REAL
(Arg p3) - 0 is complex real ext-real Element of REAL
0 + ((Arg p3) - 0) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (angle (p2,p3)) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + ((Arg p3) - (Arg p2)) is complex real ext-real Element of REAL
(Arg p3) - 0 is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + ((Arg p3) - 0) is complex real ext-real Element of REAL
Arg p3 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p3) - (Arg p2) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
(Arg p3) - (Arg p1) is complex real ext-real Element of REAL
Arg p3 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p3) - (Arg p2) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
(Arg p3) - (Arg p1) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (Arg p3) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (Arg p2) is complex real ext-real Element of REAL
(((2 * PI) - (Arg p1)) + (Arg p2)) + (angle (p2,p3)) is complex real ext-real Element of REAL
(2 * PI) - (Arg p2) is complex real ext-real Element of REAL
((2 * PI) - (Arg p2)) + (Arg p3) is complex real ext-real Element of REAL
(((2 * PI) - (Arg p1)) + (Arg p2)) + (((2 * PI) - (Arg p2)) + (Arg p3)) is complex real ext-real Element of REAL
(2 * PI) + (2 * PI) is non empty complex real ext-real positive non negative Element of REAL
((2 * PI) + (2 * PI)) - (Arg p1) is complex real ext-real Element of REAL
(((2 * PI) + (2 * PI)) - (Arg p1)) + (Arg p3) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
((Arg p2) - (Arg p1)) + (angle (p2,p3)) is complex real ext-real Element of REAL
(2 * PI) - (Arg p2) is complex real ext-real Element of REAL
((2 * PI) - (Arg p2)) + (Arg p3) is complex real ext-real Element of REAL
((Arg p2) - (Arg p1)) + (((2 * PI) - (Arg p2)) + (Arg p3)) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (Arg p3) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
Arg p3 is complex real ext-real Element of REAL
Arg p2 is complex real ext-real Element of REAL
(Arg p3) - (Arg p2) is complex real ext-real Element of REAL
Arg p1 is complex real ext-real Element of REAL
(Arg p3) - (Arg p1) is complex real ext-real Element of REAL
(Arg p2) - (Arg p1) is complex real ext-real Element of REAL
(2 * PI) - (Arg p1) is complex real ext-real Element of REAL
((2 * PI) - (Arg p1)) + (Arg p2) is complex real ext-real Element of REAL
(((2 * PI) - (Arg p1)) + (Arg p2)) + (angle (p2,p3)) is complex real ext-real Element of REAL
(((2 * PI)