:: 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)