K110() is non empty V31() V119() V120() V121() V125() set
K114() is V119() V120() V121() V122() V123() V124() V125() Element of bool K110()
bool K110() is non empty set
K92() is V119() V120() V121() V122() V123() V124() V125() set
bool K92() is non empty set
bool K114() is non empty set
K111() is non empty V31() V119() V125() set
K112() is non empty V31() V119() V120() V121() V122() V125() set
K113() is non empty V31() V119() V120() V121() V122() V123() V125() set
1 is ext-real positive non negative non empty V30() V66() V67() V68() V69() V119() V120() V121() V122() V123() V124() Element of K114()
[:1,1:] is non empty V11(K112()) V11(K113()) V109() V110() V111() V112() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty V11(K112()) V11(K113()) V109() V110() V111() V112() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],K110():] is non empty V109() V110() V111() set
bool [:[:1,1:],K110():] is non empty set
[:K110(),K110():] is non empty V109() V110() V111() set
[:[:K110(),K110():],K110():] is non empty V109() V110() V111() set
bool [:[:K110(),K110():],K110():] is non empty set
2 is ext-real positive non negative non empty V30() V66() V67() V68() V69() V119() V120() V121() V122() V123() V124() Element of K114()
[:2,2:] is non empty V11(K112()) V11(K113()) V109() V110() V111() V112() set
[:[:2,2:],K110():] is non empty V109() V110() V111() set
bool [:[:2,2:],K110():] is non empty set
bool [:K110(),K110():] is non empty set
TOP-REAL 2 is non empty TopSpace-like V85() V146() V147() V148() V149() V150() V151() V152() strict V203() V204() RLTopStruct
the U1 of (TOP-REAL 2) is non empty set
[:K111(),K111():] is non empty V109() set
bool [:K111(),K111():] is non empty set
[:[:K111(),K111():],K111():] is non empty V109() set
bool [:[:K111(),K111():],K111():] is non empty set
[:K112(),K112():] is non empty V11(K112()) V109() V110() V111() set
bool [:K112(),K112():] is non empty set
[:[:K112(),K112():],K112():] is non empty V11(K112()) V109() V110() V111() set
bool [:[:K112(),K112():],K112():] is non empty set
[:K113(),K113():] is non empty V11(K112()) V11(K113()) V109() V110() V111() set
bool [:K113(),K113():] is non empty set
[:[:K113(),K113():],K113():] is non empty V11(K112()) V11(K113()) V109() V110() V111() set
bool [:[:K113(),K113():],K113():] is non empty set
[:K114(),K114():] is V11(K112()) V11(K113()) V109() V110() V111() V112() set
[:[:K114(),K114():],K114():] is V11(K112()) V11(K113()) V109() V110() V111() V112() set
bool [:[:K114(),K114():],K114():] is non empty set
[:K114(),K110():] is V109() V110() V111() set
bool [:K114(),K110():] is non empty set
[:K114(),K111():] is V109() set
bool [:K114(),K111():] is non empty set
K473() is non empty strict TopSpace-like V182() TopStruct
the U1 of K473() is non empty V119() V120() V121() set
K281() is non empty V133() V138() V139() V140() V141() V143() V182() L13()
K478() is non empty strict TopSpace-like V182() TopStruct
the U1 of K478() is non empty V119() V120() V121() set
[: the U1 of (TOP-REAL 2), the U1 of K478():] is non empty V109() V110() V111() set
bool [: the U1 of (TOP-REAL 2), the U1 of K478():] is non empty set
K533() is non empty V87() L9()
the U1 of K533() is non empty set
K538() is non empty V87() V183() V184() V185() V187() V213() V214() V215() V216() V217() V218() L9()
K539() is non empty V87() V185() V187() V216() V217() V218() M20(K538())
K540() is non empty V87() V183() V185() V187() V216() V217() V218() V219() M23(K538(),K539())
K542() is non empty V87() V183() V185() V187() L9()
K543() is non empty V87() V183() V185() V187() V219() M20(K542())
{} is empty V119() V120() V121() V122() V123() V124() V125() set
0. (TOP-REAL 2) is V7() V12() V38(2) V47( TOP-REAL 2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
0 is ext-real non positive non negative empty V30() V66() V67() V68() V69() V119() V120() V121() V122() V123() V124() V125() Element of K114()
|[0,0]| is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
PI is ext-real positive non negative non empty V66() V67() Element of K110()
2 * PI is ext-real positive non negative non empty V66() V67() Element of K110()
bool the U1 of (TOP-REAL 2) is non empty set
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A `1 is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A + B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K512(A,B) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
(A + B) `1 is ext-real V66() V67() Element of K110()
B `1 is ext-real V66() V67() Element of K110()
(A `1) + (B `1) is ext-real V66() V67() Element of K110()
(A + B) `2 is ext-real V66() V67() Element of K110()
B `2 is ext-real V66() V67() Element of K110()
(A `2) + (B `2) is ext-real V66() V67() Element of K110()
|[((A `1) + (B `1)),((A `2) + (B `2))]| is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A `1 is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
B is ext-real V66() V67() Element of K110()
B * A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(A,B) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
(B * A) `1 is ext-real V66() V67() Element of K110()
B * (A `1) is ext-real V66() V67() Element of K110()
(B * A) `2 is ext-real V66() V67() Element of K110()
B * (A `2) is ext-real V66() V67() Element of K110()
|[(B * (A `1)),(B * (A `2))]| is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
- A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K514(A) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
(- A) `1 is ext-real V66() V67() Element of K110()
A `1 is ext-real V66() V67() Element of K110()
- (A `1) is ext-real V66() V67() Element of K110()
(- A) `2 is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
- (A `2) is ext-real V66() V67() Element of K110()
|[(- (A `1)),(- (A `2))]| is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A `1 is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
B `1 is ext-real V66() V67() Element of K110()
B `2 is ext-real V66() V67() Element of K110()
C is ext-real V66() V67() Element of K110()
C * A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(A,C) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
C * (A `1) is ext-real V66() V67() Element of K110()
C * (A `2) is ext-real V66() V67() Element of K110()
A1 is ext-real V66() V67() Element of K110()
A1 * B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(B,A1) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
(C * A) + (A1 * B) is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K512((C * A),(A1 * B)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
((C * A) + (A1 * B)) `1 is ext-real V66() V67() Element of K110()
A1 * (B `1) is ext-real V66() V67() Element of K110()
(C * (A `1)) + (A1 * (B `1)) is ext-real V66() V67() Element of K110()
((C * A) + (A1 * B)) `2 is ext-real V66() V67() Element of K110()
A1 * (B `2) is ext-real V66() V67() Element of K110()
(C * (A `2)) + (A1 * (B `2)) is ext-real V66() V67() Element of K110()
(C * A) `1 is ext-real V66() V67() Element of K110()
(A1 * B) `1 is ext-real V66() V67() Element of K110()
((C * A) `1) + ((A1 * B) `1) is ext-real V66() V67() Element of K110()
(C * (A `1)) + ((A1 * B) `1) is ext-real V66() V67() Element of K110()
(C * A) `2 is ext-real V66() V67() Element of K110()
(A1 * B) `2 is ext-real V66() V67() Element of K110()
((C * A) `2) + ((A1 * B) `2) is ext-real V66() V67() Element of K110()
(C * (A `2)) + ((A1 * B) `2) is ext-real V66() V67() Element of K110()
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A `1 is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
B is ext-real V66() V67() Element of K110()
- B is ext-real V66() V67() Element of K110()
(- B) * A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(A,(- B)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
((- B) * A) `1 is ext-real V66() V67() Element of K110()
B * (A `1) is ext-real V66() V67() Element of K110()
- (B * (A `1)) is ext-real V66() V67() Element of K110()
((- B) * A) `2 is ext-real V66() V67() Element of K110()
B * (A `2) is ext-real V66() V67() Element of K110()
- (B * (A `2)) is ext-real V66() V67() Element of K110()
B * A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(A,B) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
- (B * A) is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K514((B * A)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
(- (B * A)) `1 is ext-real V66() V67() Element of K110()
(B * A) `1 is ext-real V66() V67() Element of K110()
- ((B * A) `1) is ext-real V66() V67() Element of K110()
(- (B * A)) `2 is ext-real V66() V67() Element of K110()
(B * A) `2 is ext-real V66() V67() Element of K110()
- ((B * A) `2) is ext-real V66() V67() Element of K110()
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A `1 is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
B `1 is ext-real V66() V67() Element of K110()
B `2 is ext-real V66() V67() Element of K110()
C is ext-real V66() V67() Element of K110()
C * A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(A,C) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
C * (A `1) is ext-real V66() V67() Element of K110()
C * (A `2) is ext-real V66() V67() Element of K110()
A1 is ext-real V66() V67() Element of K110()
A1 * B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(B,A1) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
(C * A) - (A1 * B) is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K516((C * A),(A1 * B)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
((C * A) - (A1 * B)) `1 is ext-real V66() V67() Element of K110()
A1 * (B `1) is ext-real V66() V67() Element of K110()
(C * (A `1)) - (A1 * (B `1)) is ext-real V66() V67() Element of K110()
((C * A) - (A1 * B)) `2 is ext-real V66() V67() Element of K110()
A1 * (B `2) is ext-real V66() V67() Element of K110()
(C * (A `2)) - (A1 * (B `2)) is ext-real V66() V67() Element of K110()
(C * A) `1 is ext-real V66() V67() Element of K110()
(A1 * B) `1 is ext-real V66() V67() Element of K110()
((C * A) `1) - ((A1 * B) `1) is ext-real V66() V67() Element of K110()
(C * (A `1)) - ((A1 * B) `1) is ext-real V66() V67() Element of K110()
(C * A) `2 is ext-real V66() V67() Element of K110()
(A1 * B) `2 is ext-real V66() V67() Element of K110()
((C * A) `2) - ((A1 * B) `2) is ext-real V66() V67() Element of K110()
(C * (A `2)) - ((A1 * B) `2) is ext-real V66() V67() Element of K110()
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
C is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A1 is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
the_area_of_polygon3 (A,C,A1) is ext-real V66() V67() set
A `1 is ext-real V66() V67() Element of K110()
C `2 is ext-real V66() V67() Element of K110()
(A `1) * (C `2) is ext-real V66() V67() Element of K110()
C `1 is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
(C `1) * (A `2) is ext-real V66() V67() Element of K110()
((A `1) * (C `2)) - ((C `1) * (A `2)) is ext-real V66() V67() Element of K110()
A1 `2 is ext-real V66() V67() Element of K110()
(C `1) * (A1 `2) is ext-real V66() V67() Element of K110()
A1 `1 is ext-real V66() V67() Element of K110()
(A1 `1) * (C `2) is ext-real V66() V67() Element of K110()
((C `1) * (A1 `2)) - ((A1 `1) * (C `2)) is ext-real V66() V67() Element of K110()
(((A `1) * (C `2)) - ((C `1) * (A `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2))) is ext-real V66() V67() Element of K110()
(A1 `1) * (A `2) is ext-real V66() V67() Element of K110()
(A `1) * (A1 `2) is ext-real V66() V67() Element of K110()
((A1 `1) * (A `2)) - ((A `1) * (A1 `2)) is ext-real V66() V67() Element of K110()
((((A `1) * (C `2)) - ((C `1) * (A `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (A `2)) - ((A `1) * (A1 `2))) is ext-real V66() V67() Element of K110()
(((((A `1) * (C `2)) - ((C `1) * (A `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (A `2)) - ((A `1) * (A1 `2)))) / 2 is ext-real V66() V67() Element of K110()
the_area_of_polygon3 (B,C,A1) is ext-real V66() V67() set
B `1 is ext-real V66() V67() Element of K110()
(B `1) * (C `2) is ext-real V66() V67() Element of K110()
B `2 is ext-real V66() V67() Element of K110()
(C `1) * (B `2) is ext-real V66() V67() Element of K110()
((B `1) * (C `2)) - ((C `1) * (B `2)) is ext-real V66() V67() Element of K110()
(((B `1) * (C `2)) - ((C `1) * (B `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2))) is ext-real V66() V67() Element of K110()
(A1 `1) * (B `2) is ext-real V66() V67() Element of K110()
(B `1) * (A1 `2) is ext-real V66() V67() Element of K110()
((A1 `1) * (B `2)) - ((B `1) * (A1 `2)) is ext-real V66() V67() Element of K110()
((((B `1) * (C `2)) - ((C `1) * (B `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (B `2)) - ((B `1) * (A1 `2))) is ext-real V66() V67() Element of K110()
(((((B `1) * (C `2)) - ((C `1) * (B `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (B `2)) - ((B `1) * (A1 `2)))) / 2 is ext-real V66() V67() Element of K110()
B1 is ext-real V66() V67() Element of K110()
1 - B1 is ext-real V66() V67() Element of K110()
(1 - B1) * A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(A,(1 - B1)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
B1 * B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(B,B1) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
((1 - B1) * A) + (B1 * B) is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K512(((1 - B1) * A),(B1 * B)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
the_area_of_polygon3 ((((1 - B1) * A) + (B1 * B)),C,A1) is ext-real V66() V67() set
(((1 - B1) * A) + (B1 * B)) `1 is ext-real V66() V67() Element of K110()
((((1 - B1) * A) + (B1 * B)) `1) * (C `2) is ext-real V66() V67() Element of K110()
(((1 - B1) * A) + (B1 * B)) `2 is ext-real V66() V67() Element of K110()
(C `1) * ((((1 - B1) * A) + (B1 * B)) `2) is ext-real V66() V67() Element of K110()
(((((1 - B1) * A) + (B1 * B)) `1) * (C `2)) - ((C `1) * ((((1 - B1) * A) + (B1 * B)) `2)) is ext-real V66() V67() Element of K110()
((((((1 - B1) * A) + (B1 * B)) `1) * (C `2)) - ((C `1) * ((((1 - B1) * A) + (B1 * B)) `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2))) is ext-real V66() V67() Element of K110()
(A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2) is ext-real V66() V67() Element of K110()
((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2) is ext-real V66() V67() Element of K110()
((A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2)) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2)) is ext-real V66() V67() Element of K110()
(((((((1 - B1) * A) + (B1 * B)) `1) * (C `2)) - ((C `1) * ((((1 - B1) * A) + (B1 * B)) `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2)) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2))) is ext-real V66() V67() Element of K110()
((((((((1 - B1) * A) + (B1 * B)) `1) * (C `2)) - ((C `1) * ((((1 - B1) * A) + (B1 * B)) `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2)) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2)))) / 2 is ext-real V66() V67() Element of K110()
(1 - B1) * (the_area_of_polygon3 (A,C,A1)) is ext-real V66() V67() Element of K110()
B1 * (the_area_of_polygon3 (B,C,A1)) is ext-real V66() V67() Element of K110()
((1 - B1) * (the_area_of_polygon3 (A,C,A1))) + (B1 * (the_area_of_polygon3 (B,C,A1))) is ext-real V66() V67() Element of K110()
(1 - B1) * (A `1) is ext-real V66() V67() Element of K110()
B1 * (B `1) is ext-real V66() V67() Element of K110()
((1 - B1) * (A `1)) + (B1 * (B `1)) is ext-real V66() V67() Element of K110()
(((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2) is ext-real V66() V67() Element of K110()
(C `1) * ((((1 - B1) * A) + (B1 * B)) `2) is ext-real V66() V67() Element of K110()
((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * ((((1 - B1) * A) + (B1 * B)) `2)) is ext-real V66() V67() Element of K110()
(C `1) * (A1 `2) is ext-real V66() V67() Element of K110()
(A1 `1) * (C `2) is ext-real V66() V67() Element of K110()
((C `1) * (A1 `2)) - ((A1 `1) * (C `2)) is ext-real V66() V67() Element of K110()
(((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * ((((1 - B1) * A) + (B1 * B)) `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2))) is ext-real V66() V67() Element of K110()
(A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2) is ext-real V66() V67() Element of K110()
((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2) is ext-real V66() V67() Element of K110()
((A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2)) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2)) is ext-real V66() V67() Element of K110()
((((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * ((((1 - B1) * A) + (B1 * B)) `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2)) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2))) is ext-real V66() V67() Element of K110()
(((((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * ((((1 - B1) * A) + (B1 * B)) `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2)) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2)))) / 2 is ext-real V66() V67() Element of K110()
(1 - B1) * (A `2) is ext-real V66() V67() Element of K110()
B1 * (B `2) is ext-real V66() V67() Element of K110()
((1 - B1) * (A `2)) + (B1 * (B `2)) is ext-real V66() V67() Element of K110()
(C `1) * (((1 - B1) * (A `2)) + (B1 * (B `2))) is ext-real V66() V67() Element of K110()
((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * (((1 - B1) * (A `2)) + (B1 * (B `2)))) is ext-real V66() V67() Element of K110()
(((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * (((1 - B1) * (A `2)) + (B1 * (B `2))))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2))) is ext-real V66() V67() Element of K110()
((((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * (((1 - B1) * (A `2)) + (B1 * (B `2))))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2)) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2))) is ext-real V66() V67() Element of K110()
(((((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * (((1 - B1) * (A `2)) + (B1 * (B `2))))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * ((((1 - B1) * A) + (B1 * B)) `2)) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2)))) / 2 is ext-real V66() V67() Element of K110()
(A1 `1) * (((1 - B1) * (A `2)) + (B1 * (B `2))) is ext-real V66() V67() Element of K110()
((A1 `1) * (((1 - B1) * (A `2)) + (B1 * (B `2)))) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2)) is ext-real V66() V67() Element of K110()
((((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * (((1 - B1) * (A `2)) + (B1 * (B `2))))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (((1 - B1) * (A `2)) + (B1 * (B `2)))) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2))) is ext-real V66() V67() Element of K110()
(((((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * (((1 - B1) * (A `2)) + (B1 * (B `2))))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (((1 - B1) * (A `2)) + (B1 * (B `2)))) - (((((1 - B1) * A) + (B1 * B)) `1) * (A1 `2)))) / 2 is ext-real V66() V67() Element of K110()
(((1 - B1) * (A `1)) + (B1 * (B `1))) * (A1 `2) is ext-real V66() V67() Element of K110()
((A1 `1) * (((1 - B1) * (A `2)) + (B1 * (B `2)))) - ((((1 - B1) * (A `1)) + (B1 * (B `1))) * (A1 `2)) is ext-real V66() V67() Element of K110()
((((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * (((1 - B1) * (A `2)) + (B1 * (B `2))))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (((1 - B1) * (A `2)) + (B1 * (B `2)))) - ((((1 - B1) * (A `1)) + (B1 * (B `1))) * (A1 `2))) is ext-real V66() V67() Element of K110()
(((((((1 - B1) * (A `1)) + (B1 * (B `1))) * (C `2)) - ((C `1) * (((1 - B1) * (A `2)) + (B1 * (B `2))))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (((1 - B1) * (A `2)) + (B1 * (B `2)))) - ((((1 - B1) * (A `1)) + (B1 * (B `1))) * (A1 `2)))) / 2 is ext-real V66() V67() Element of K110()
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
C is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
angle (A,B,C) is ext-real V66() V67() Element of K110()
euc2cpx A is V66() Element of K111()
euc2cpx B is V66() Element of K111()
euc2cpx C is V66() Element of K111()
angle ((euc2cpx A),(euc2cpx B),(euc2cpx C)) is ext-real V66() V67() set
angle (B,C,A) is ext-real V66() V67() Element of K110()
angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) is ext-real V66() V67() set
angle (B,A,C) is ext-real V66() V67() Element of K110()
angle ((euc2cpx B),(euc2cpx A),(euc2cpx C)) is ext-real V66() V67() set
angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) is ext-real V66() V67() set
angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) is ext-real V66() V67() set
angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) is ext-real V66() V67() set
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
C is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
the_area_of_polygon3 (A,B,C) is ext-real V66() V67() set
A `1 is ext-real V66() V67() Element of K110()
B `2 is ext-real V66() V67() Element of K110()
(A `1) * (B `2) is ext-real V66() V67() Element of K110()
B `1 is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
(B `1) * (A `2) is ext-real V66() V67() Element of K110()
((A `1) * (B `2)) - ((B `1) * (A `2)) is ext-real V66() V67() Element of K110()
C `2 is ext-real V66() V67() Element of K110()
(B `1) * (C `2) is ext-real V66() V67() Element of K110()
C `1 is ext-real V66() V67() Element of K110()
(C `1) * (B `2) is ext-real V66() V67() Element of K110()
((B `1) * (C `2)) - ((C `1) * (B `2)) is ext-real V66() V67() Element of K110()
(((A `1) * (B `2)) - ((B `1) * (A `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2))) is ext-real V66() V67() Element of K110()
(C `1) * (A `2) is ext-real V66() V67() Element of K110()
(A `1) * (C `2) is ext-real V66() V67() Element of K110()
((C `1) * (A `2)) - ((A `1) * (C `2)) is ext-real V66() V67() Element of K110()
((((A `1) * (B `2)) - ((B `1) * (A `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (A `2)) - ((A `1) * (C `2))) is ext-real V66() V67() Element of K110()
(((((A `1) * (B `2)) - ((B `1) * (A `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (A `2)) - ((A `1) * (C `2)))) / 2 is ext-real V66() V67() Element of K110()
LSeg (B,C) is Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * B) + (b1 * C)) where b1 is ext-real V66() V67() Element of K110() : ( 0 <= b1 & b1 <= 1 ) } is set
A1 is ext-real V66() V67() Element of K110()
1 - A1 is ext-real V66() V67() Element of K110()
(1 - A1) * B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(B,(1 - A1)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
A1 * C is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(C,A1) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
((1 - A1) * B) + (A1 * C) is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K512(((1 - A1) * B),(A1 * C)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
the_area_of_polygon3 (B,B,C) is ext-real V66() V67() set
(B `1) * (B `2) is ext-real V66() V67() Element of K110()
((B `1) * (B `2)) - ((B `1) * (B `2)) is ext-real V66() V67() Element of K110()
(((B `1) * (B `2)) - ((B `1) * (B `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2))) is ext-real V66() V67() Element of K110()
((C `1) * (B `2)) - ((B `1) * (C `2)) is ext-real V66() V67() Element of K110()
((((B `1) * (B `2)) - ((B `1) * (B `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (B `2)) - ((B `1) * (C `2))) is ext-real V66() V67() Element of K110()
(((((B `1) * (B `2)) - ((B `1) * (B `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (B `2)) - ((B `1) * (C `2)))) / 2 is ext-real V66() V67() Element of K110()
(1 - A1) * (the_area_of_polygon3 (B,B,C)) is ext-real V66() V67() Element of K110()
the_area_of_polygon3 (C,B,C) is ext-real V66() V67() set
(((C `1) * (B `2)) - ((B `1) * (C `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2))) is ext-real V66() V67() Element of K110()
(C `1) * (C `2) is ext-real V66() V67() Element of K110()
((C `1) * (C `2)) - ((C `1) * (C `2)) is ext-real V66() V67() Element of K110()
((((C `1) * (B `2)) - ((B `1) * (C `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (C `2)) - ((C `1) * (C `2))) is ext-real V66() V67() Element of K110()
(((((C `1) * (B `2)) - ((B `1) * (C `2))) + (((B `1) * (C `2)) - ((C `1) * (B `2)))) + (((C `1) * (C `2)) - ((C `1) * (C `2)))) / 2 is ext-real V66() V67() Element of K110()
A1 * (the_area_of_polygon3 (C,B,C)) is ext-real V66() V67() Element of K110()
((1 - A1) * (the_area_of_polygon3 (B,B,C))) + (A1 * (the_area_of_polygon3 (C,B,C))) is ext-real V66() V67() Element of K110()
LSeg (C,A) is Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * C) + (b1 * A)) where b1 is ext-real V66() V67() Element of K110() : ( 0 <= b1 & b1 <= 1 ) } is set
A1 is ext-real V66() V67() Element of K110()
1 - A1 is ext-real V66() V67() Element of K110()
(1 - A1) * C is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(C,(1 - A1)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
A1 * A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(A,A1) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
((1 - A1) * C) + (A1 * A) is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K512(((1 - A1) * C),(A1 * A)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
the_area_of_polygon3 ((((1 - A1) * C) + (A1 * A)),A,C) is ext-real V66() V67() set
(((1 - A1) * C) + (A1 * A)) `1 is ext-real V66() V67() Element of K110()
((((1 - A1) * C) + (A1 * A)) `1) * (A `2) is ext-real V66() V67() Element of K110()
(((1 - A1) * C) + (A1 * A)) `2 is ext-real V66() V67() Element of K110()
(A `1) * ((((1 - A1) * C) + (A1 * A)) `2) is ext-real V66() V67() Element of K110()
(((((1 - A1) * C) + (A1 * A)) `1) * (A `2)) - ((A `1) * ((((1 - A1) * C) + (A1 * A)) `2)) is ext-real V66() V67() Element of K110()
((A `1) * (C `2)) - ((C `1) * (A `2)) is ext-real V66() V67() Element of K110()
((((((1 - A1) * C) + (A1 * A)) `1) * (A `2)) - ((A `1) * ((((1 - A1) * C) + (A1 * A)) `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2))) is ext-real V66() V67() Element of K110()
(C `1) * ((((1 - A1) * C) + (A1 * A)) `2) is ext-real V66() V67() Element of K110()
((((1 - A1) * C) + (A1 * A)) `1) * (C `2) is ext-real V66() V67() Element of K110()
((C `1) * ((((1 - A1) * C) + (A1 * A)) `2)) - (((((1 - A1) * C) + (A1 * A)) `1) * (C `2)) is ext-real V66() V67() Element of K110()
(((((((1 - A1) * C) + (A1 * A)) `1) * (A `2)) - ((A `1) * ((((1 - A1) * C) + (A1 * A)) `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2)))) + (((C `1) * ((((1 - A1) * C) + (A1 * A)) `2)) - (((((1 - A1) * C) + (A1 * A)) `1) * (C `2))) is ext-real V66() V67() Element of K110()
((((((((1 - A1) * C) + (A1 * A)) `1) * (A `2)) - ((A `1) * ((((1 - A1) * C) + (A1 * A)) `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2)))) + (((C `1) * ((((1 - A1) * C) + (A1 * A)) `2)) - (((((1 - A1) * C) + (A1 * A)) `1) * (C `2)))) / 2 is ext-real V66() V67() Element of K110()
- (the_area_of_polygon3 ((((1 - A1) * C) + (A1 * A)),A,C)) is ext-real V66() V67() Element of K110()
the_area_of_polygon3 (C,A,C) is ext-real V66() V67() set
(((C `1) * (A `2)) - ((A `1) * (C `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2))) is ext-real V66() V67() Element of K110()
(C `1) * (C `2) is ext-real V66() V67() Element of K110()
((C `1) * (C `2)) - ((C `1) * (C `2)) is ext-real V66() V67() Element of K110()
((((C `1) * (A `2)) - ((A `1) * (C `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2)))) + (((C `1) * (C `2)) - ((C `1) * (C `2))) is ext-real V66() V67() Element of K110()
(((((C `1) * (A `2)) - ((A `1) * (C `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2)))) + (((C `1) * (C `2)) - ((C `1) * (C `2)))) / 2 is ext-real V66() V67() Element of K110()
(1 - A1) * (the_area_of_polygon3 (C,A,C)) is ext-real V66() V67() Element of K110()
- ((1 - A1) * (the_area_of_polygon3 (C,A,C))) is ext-real V66() V67() Element of K110()
the_area_of_polygon3 (A,A,C) is ext-real V66() V67() set
(A `1) * (A `2) is ext-real V66() V67() Element of K110()
((A `1) * (A `2)) - ((A `1) * (A `2)) is ext-real V66() V67() Element of K110()
(((A `1) * (A `2)) - ((A `1) * (A `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2))) is ext-real V66() V67() Element of K110()
((((A `1) * (A `2)) - ((A `1) * (A `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2)))) + (((C `1) * (A `2)) - ((A `1) * (C `2))) is ext-real V66() V67() Element of K110()
(((((A `1) * (A `2)) - ((A `1) * (A `2))) + (((A `1) * (C `2)) - ((C `1) * (A `2)))) + (((C `1) * (A `2)) - ((A `1) * (C `2)))) / 2 is ext-real V66() V67() Element of K110()
A1 * (the_area_of_polygon3 (A,A,C)) is ext-real V66() V67() Element of K110()
(- ((1 - A1) * (the_area_of_polygon3 (C,A,C)))) - (A1 * (the_area_of_polygon3 (A,A,C))) is ext-real V66() V67() Element of K110()
LSeg (A,B) is Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * A) + (b1 * B)) where b1 is ext-real V66() V67() Element of K110() : ( 0 <= b1 & b1 <= 1 ) } is set
A1 is ext-real V66() V67() Element of K110()
1 - A1 is ext-real V66() V67() Element of K110()
(1 - A1) * A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(A,(1 - A1)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
A1 * B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K518(B,A1) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
((1 - A1) * A) + (A1 * B) is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K512(((1 - A1) * A),(A1 * B)) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
the_area_of_polygon3 ((((1 - A1) * A) + (A1 * B)),B,A) is ext-real V66() V67() set
(((1 - A1) * A) + (A1 * B)) `1 is ext-real V66() V67() Element of K110()
((((1 - A1) * A) + (A1 * B)) `1) * (B `2) is ext-real V66() V67() Element of K110()
(((1 - A1) * A) + (A1 * B)) `2 is ext-real V66() V67() Element of K110()
(B `1) * ((((1 - A1) * A) + (A1 * B)) `2) is ext-real V66() V67() Element of K110()
(((((1 - A1) * A) + (A1 * B)) `1) * (B `2)) - ((B `1) * ((((1 - A1) * A) + (A1 * B)) `2)) is ext-real V66() V67() Element of K110()
((B `1) * (A `2)) - ((A `1) * (B `2)) is ext-real V66() V67() Element of K110()
((((((1 - A1) * A) + (A1 * B)) `1) * (B `2)) - ((B `1) * ((((1 - A1) * A) + (A1 * B)) `2))) + (((B `1) * (A `2)) - ((A `1) * (B `2))) is ext-real V66() V67() Element of K110()
(A `1) * ((((1 - A1) * A) + (A1 * B)) `2) is ext-real V66() V67() Element of K110()
((((1 - A1) * A) + (A1 * B)) `1) * (A `2) is ext-real V66() V67() Element of K110()
((A `1) * ((((1 - A1) * A) + (A1 * B)) `2)) - (((((1 - A1) * A) + (A1 * B)) `1) * (A `2)) is ext-real V66() V67() Element of K110()
(((((((1 - A1) * A) + (A1 * B)) `1) * (B `2)) - ((B `1) * ((((1 - A1) * A) + (A1 * B)) `2))) + (((B `1) * (A `2)) - ((A `1) * (B `2)))) + (((A `1) * ((((1 - A1) * A) + (A1 * B)) `2)) - (((((1 - A1) * A) + (A1 * B)) `1) * (A `2))) is ext-real V66() V67() Element of K110()
((((((((1 - A1) * A) + (A1 * B)) `1) * (B `2)) - ((B `1) * ((((1 - A1) * A) + (A1 * B)) `2))) + (((B `1) * (A `2)) - ((A `1) * (B `2)))) + (((A `1) * ((((1 - A1) * A) + (A1 * B)) `2)) - (((((1 - A1) * A) + (A1 * B)) `1) * (A `2)))) / 2 is ext-real V66() V67() Element of K110()
- (the_area_of_polygon3 ((((1 - A1) * A) + (A1 * B)),B,A)) is ext-real V66() V67() Element of K110()
the_area_of_polygon3 (A,B,A) is ext-real V66() V67() set
(((A `1) * (B `2)) - ((B `1) * (A `2))) + (((B `1) * (A `2)) - ((A `1) * (B `2))) is ext-real V66() V67() Element of K110()
(A `1) * (A `2) is ext-real V66() V67() Element of K110()
((A `1) * (A `2)) - ((A `1) * (A `2)) is ext-real V66() V67() Element of K110()
((((A `1) * (B `2)) - ((B `1) * (A `2))) + (((B `1) * (A `2)) - ((A `1) * (B `2)))) + (((A `1) * (A `2)) - ((A `1) * (A `2))) is ext-real V66() V67() Element of K110()
(((((A `1) * (B `2)) - ((B `1) * (A `2))) + (((B `1) * (A `2)) - ((A `1) * (B `2)))) + (((A `1) * (A `2)) - ((A `1) * (A `2)))) / 2 is ext-real V66() V67() Element of K110()
(1 - A1) * (the_area_of_polygon3 (A,B,A)) is ext-real V66() V67() Element of K110()
- ((1 - A1) * (the_area_of_polygon3 (A,B,A))) is ext-real V66() V67() Element of K110()
the_area_of_polygon3 (B,B,A) is ext-real V66() V67() set
(B `1) * (B `2) is ext-real V66() V67() Element of K110()
((B `1) * (B `2)) - ((B `1) * (B `2)) is ext-real V66() V67() Element of K110()
(((B `1) * (B `2)) - ((B `1) * (B `2))) + (((B `1) * (A `2)) - ((A `1) * (B `2))) is ext-real V66() V67() Element of K110()
((((B `1) * (B `2)) - ((B `1) * (B `2))) + (((B `1) * (A `2)) - ((A `1) * (B `2)))) + (((A `1) * (B `2)) - ((B `1) * (A `2))) is ext-real V66() V67() Element of K110()
(((((B `1) * (B `2)) - ((B `1) * (B `2))) + (((B `1) * (A `2)) - ((A `1) * (B `2)))) + (((A `1) * (B `2)) - ((B `1) * (A `2)))) / 2 is ext-real V66() V67() Element of K110()
A1 * (the_area_of_polygon3 (B,B,A)) is ext-real V66() V67() Element of K110()
(- ((1 - A1) * (the_area_of_polygon3 (A,B,A)))) - (A1 * (the_area_of_polygon3 (B,B,A))) is ext-real V66() V67() Element of K110()
LSeg (B,C) is Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * B) + (b1 * C)) where b1 is ext-real V66() V67() Element of K110() : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (C,A) is Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * C) + (b1 * A)) where b1 is ext-real V66() V67() Element of K110() : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (A,B) is Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * A) + (b1 * B)) where b1 is ext-real V66() V67() Element of K110() : ( 0 <= b1 & b1 <= 1 ) } is set
A - B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K516(A,B) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
|.(A - B).| is ext-real non negative V66() V67() Element of K110()
C - B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K516(C,B) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
|.(C - B).| is ext-real non negative V66() V67() Element of K110()
|.(A - B).| * |.(C - B).| is ext-real non negative V66() V67() Element of K110()
angle (C,B,A) is ext-real V66() V67() Element of K110()
euc2cpx C is V66() Element of K111()
euc2cpx B is V66() Element of K111()
euc2cpx A is V66() Element of K111()
angle ((euc2cpx C),(euc2cpx B),(euc2cpx A)) is ext-real V66() V67() set
sin (angle (C,B,A)) is ext-real V66() V67() Element of K110()
(|.(A - B).| * |.(C - B).|) * (sin (angle (C,B,A))) is ext-real V66() V67() Element of K110()
((|.(A - B).| * |.(C - B).|) * (sin (angle (C,B,A)))) / 2 is ext-real V66() V67() Element of K110()
2 * PI is ext-real positive non negative non empty V66() V67() Element of K110()
(2 * PI) * 0 is ext-real non positive non negative empty V66() V67() V119() V120() V121() V122() V123() V124() V125() Element of K110()
(2 * PI) + ((2 * PI) * 0) is ext-real positive non negative non empty V66() V67() Element of K110()
PI + ((2 * PI) * 0) is ext-real positive non negative non empty V66() V67() Element of K110()
angle (B,C,A) is ext-real V66() V67() Element of K110()
angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) is ext-real V66() V67() set
angle (B,A,C) is ext-real V66() V67() Element of K110()
angle ((euc2cpx B),(euc2cpx A),(euc2cpx C)) is ext-real V66() V67() set
LSeg (B,A) is Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * B) + (b1 * A)) where b1 is ext-real V66() V67() Element of K110() : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (B,C) is Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * B) + (b1 * C)) where b1 is ext-real V66() V67() Element of K110() : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (C,A) is Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * C) + (b1 * A)) where b1 is ext-real V66() V67() Element of K110() : ( 0 <= b1 & b1 <= 1 ) } is set
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A `1 is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
the_area_of_polygon3 ((0. (TOP-REAL 2)),A,B) is ext-real V66() V67() set
(0. (TOP-REAL 2)) `1 is ext-real V66() V67() Element of K110()
((0. (TOP-REAL 2)) `1) * (A `2) is ext-real V66() V67() Element of K110()
(0. (TOP-REAL 2)) `2 is ext-real V66() V67() Element of K110()
(A `1) * ((0. (TOP-REAL 2)) `2) is ext-real V66() V67() Element of K110()
(((0. (TOP-REAL 2)) `1) * (A `2)) - ((A `1) * ((0. (TOP-REAL 2)) `2)) is ext-real V66() V67() Element of K110()
B `2 is ext-real V66() V67() Element of K110()
(A `1) * (B `2) is ext-real V66() V67() Element of K110()
B `1 is ext-real V66() V67() Element of K110()
(B `1) * (A `2) is ext-real V66() V67() Element of K110()
((A `1) * (B `2)) - ((B `1) * (A `2)) is ext-real V66() V67() Element of K110()
((((0. (TOP-REAL 2)) `1) * (A `2)) - ((A `1) * ((0. (TOP-REAL 2)) `2))) + (((A `1) * (B `2)) - ((B `1) * (A `2))) is ext-real V66() V67() Element of K110()
(B `1) * ((0. (TOP-REAL 2)) `2) is ext-real V66() V67() Element of K110()
((0. (TOP-REAL 2)) `1) * (B `2) is ext-real V66() V67() Element of K110()
((B `1) * ((0. (TOP-REAL 2)) `2)) - (((0. (TOP-REAL 2)) `1) * (B `2)) is ext-real V66() V67() Element of K110()
(((((0. (TOP-REAL 2)) `1) * (A `2)) - ((A `1) * ((0. (TOP-REAL 2)) `2))) + (((A `1) * (B `2)) - ((B `1) * (A `2)))) + (((B `1) * ((0. (TOP-REAL 2)) `2)) - (((0. (TOP-REAL 2)) `1) * (B `2))) is ext-real V66() V67() Element of K110()
((((((0. (TOP-REAL 2)) `1) * (A `2)) - ((A `1) * ((0. (TOP-REAL 2)) `2))) + (((A `1) * (B `2)) - ((B `1) * (A `2)))) + (((B `1) * ((0. (TOP-REAL 2)) `2)) - (((0. (TOP-REAL 2)) `1) * (B `2)))) / 2 is ext-real V66() V67() Element of K110()
(A `1) * (B `2) is ext-real V66() V67() Element of K110()
(B `1) * (A `2) is ext-real V66() V67() Element of K110()
((A `1) * (B `2)) - ((B `1) * (A `2)) is ext-real V66() V67() Element of K110()
(((A `1) * (B `2)) - ((B `1) * (A `2))) / 2 is ext-real V66() V67() Element of K110()
0 * (A `2) is ext-real V66() V67() Element of K110()
|[0,0]| `2 is ext-real V66() V67() Element of K110()
(A `1) * (|[0,0]| `2) is ext-real V66() V67() Element of K110()
(0 * (A `2)) - ((A `1) * (|[0,0]| `2)) is ext-real V66() V67() Element of K110()
((0 * (A `2)) - ((A `1) * (|[0,0]| `2))) + (((A `1) * (B `2)) - ((B `1) * (A `2))) is ext-real V66() V67() Element of K110()
(B `1) * (|[0,0]| `2) is ext-real V66() V67() Element of K110()
|[0,0]| `1 is ext-real V66() V67() Element of K110()
(|[0,0]| `1) * (B `2) is ext-real V66() V67() Element of K110()
((B `1) * (|[0,0]| `2)) - ((|[0,0]| `1) * (B `2)) is ext-real V66() V67() Element of K110()
(((0 * (A `2)) - ((A `1) * (|[0,0]| `2))) + (((A `1) * (B `2)) - ((B `1) * (A `2)))) + (((B `1) * (|[0,0]| `2)) - ((|[0,0]| `1) * (B `2))) is ext-real V66() V67() Element of K110()
((((0 * (A `2)) - ((A `1) * (|[0,0]| `2))) + (((A `1) * (B `2)) - ((B `1) * (A `2)))) + (((B `1) * (|[0,0]| `2)) - ((|[0,0]| `1) * (B `2)))) / 2 is ext-real V66() V67() Element of K110()
(A `1) * 0 is ext-real V66() V67() Element of K110()
0 - ((A `1) * 0) is ext-real V66() V67() Element of K110()
(0 - ((A `1) * 0)) + (((A `1) * (B `2)) - ((B `1) * (A `2))) is ext-real V66() V67() Element of K110()
((0 - ((A `1) * 0)) + (((A `1) * (B `2)) - ((B `1) * (A `2)))) + (((B `1) * (|[0,0]| `2)) - ((|[0,0]| `1) * (B `2))) is ext-real V66() V67() Element of K110()
(((0 - ((A `1) * 0)) + (((A `1) * (B `2)) - ((B `1) * (A `2)))) + (((B `1) * (|[0,0]| `2)) - ((|[0,0]| `1) * (B `2)))) / 2 is ext-real V66() V67() Element of K110()
(B `1) * 0 is ext-real V66() V67() Element of K110()
((B `1) * 0) - ((|[0,0]| `1) * (B `2)) is ext-real V66() V67() Element of K110()
(((A `1) * (B `2)) - ((B `1) * (A `2))) + (((B `1) * 0) - ((|[0,0]| `1) * (B `2))) is ext-real V66() V67() Element of K110()
((((A `1) * (B `2)) - ((B `1) * (A `2))) + (((B `1) * 0) - ((|[0,0]| `1) * (B `2)))) / 2 is ext-real V66() V67() Element of K110()
0 * (B `2) is ext-real V66() V67() Element of K110()
0 - (0 * (B `2)) is ext-real V66() V67() Element of K110()
(((A `1) * (B `2)) - ((B `1) * (A `2))) + (0 - (0 * (B `2))) is ext-real V66() V67() Element of K110()
((((A `1) * (B `2)) - ((B `1) * (A `2))) + (0 - (0 * (B `2)))) / 2 is ext-real V66() V67() Element of K110()
A is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A + B is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
K512(A,B) is V7() V10(K114()) V11(K110()) V12() V70() V109() V110() V111() M8(K110())
C is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
A1 is V7() V12() V38(2) V70() V109() V110() V111() Element of the U1 of (TOP-REAL 2)
the_area_of_polygon3 ((A + B),C,A1) is ext-real V66() V67() set
(A + B) `1 is ext-real V66() V67() Element of K110()
C `2 is ext-real V66() V67() Element of K110()
((A + B) `1) * (C `2) is ext-real V66() V67() Element of K110()
C `1 is ext-real V66() V67() Element of K110()
(A + B) `2 is ext-real V66() V67() Element of K110()
(C `1) * ((A + B) `2) is ext-real V66() V67() Element of K110()
(((A + B) `1) * (C `2)) - ((C `1) * ((A + B) `2)) is ext-real V66() V67() Element of K110()
A1 `2 is ext-real V66() V67() Element of K110()
(C `1) * (A1 `2) is ext-real V66() V67() Element of K110()
A1 `1 is ext-real V66() V67() Element of K110()
(A1 `1) * (C `2) is ext-real V66() V67() Element of K110()
((C `1) * (A1 `2)) - ((A1 `1) * (C `2)) is ext-real V66() V67() Element of K110()
((((A + B) `1) * (C `2)) - ((C `1) * ((A + B) `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2))) is ext-real V66() V67() Element of K110()
(A1 `1) * ((A + B) `2) is ext-real V66() V67() Element of K110()
((A + B) `1) * (A1 `2) is ext-real V66() V67() Element of K110()
((A1 `1) * ((A + B) `2)) - (((A + B) `1) * (A1 `2)) is ext-real V66() V67() Element of K110()
(((((A + B) `1) * (C `2)) - ((C `1) * ((A + B) `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * ((A + B) `2)) - (((A + B) `1) * (A1 `2))) is ext-real V66() V67() Element of K110()
((((((A + B) `1) * (C `2)) - ((C `1) * ((A + B) `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * ((A + B) `2)) - (((A + B) `1) * (A1 `2)))) / 2 is ext-real V66() V67() Element of K110()
the_area_of_polygon3 (A,C,A1) is ext-real V66() V67() set
A `1 is ext-real V66() V67() Element of K110()
(A `1) * (C `2) is ext-real V66() V67() Element of K110()
A `2 is ext-real V66() V67() Element of K110()
(C `1) * (A `2) is ext-real V66() V67() Element of K110()
((A `1) * (C `2)) - ((C `1) * (A `2)) is ext-real V66() V67() Element of K110()
(((A `1) * (C `2)) - ((C `1) * (A `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2))) is ext-real V66() V67() Element of K110()
(A1 `1) * (A `2) is ext-real V66() V67() Element of K110()
(A `1) * (A1 `2) is ext-real V66() V67() Element of K110()
((A1 `1) * (A `2)) - ((A `1) * (A1 `2)) is ext-real V66() V67() Element of K110()
((((A `1) * (C `2)) - ((C `1) * (A `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (A `2)) - ((A `1) * (A1 `2))) is ext-real V66() V67() Element of K110()
(((((A `1) * (C `2)) - ((C `1) * (A `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1) * (A `2)) - ((A `1) * (A1 `2)))) / 2 is ext-real V66() V67() Element of K110()
the_area_of_polygon3 (B,C,A1) is ext-real V66() V67() set
B `1 is ext-real V66() V67() Element of K110()
(B `1) * (C `2) is ext-real V66() V67() Element of K110()
B `2 is ext-real V66() V67() Element of K110()
(C `1) * (B `2) is ext-real V66() V67() Element of K110()
((B `1) * (C `2)) - ((C `1) * (B `2)) is ext-real V66() V67() Element of K110()
(((B `1) * (C `2)) - ((C `1) * (B `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2))) is ext-real V66() V67() Element of K110()
(A1 `1) * (B `2) is ext-real V66() V67() Element of K110()
(B `1) * (A1 `2) is ext-real V66() V67() Element of K110()
((A1 `1) * (B `2)) - ((B `1) * (A1 `2)) is ext-real V66() V67() Element of K110()
((((B `1) * (C `2)) - ((C `1) * (B `2))) + (((C `1) * (A1 `2)) - ((A1 `1) * (C `2)))) + (((A1 `1)