:: METRIC_3 semantic presentation

REAL is non empty V16() V17() V18() V22() V43() set
NAT is V16() V17() V18() V19() V20() V21() V22() Element of bool REAL
bool REAL is non empty set
omega is V16() V17() V18() V19() V20() V21() V22() set
bool omega is non empty set
1 is ext-real positive non empty natural V14() real V16() V17() V18() V19() V20() V21() Element of NAT
[:1,1:] is non empty V23() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty V23() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V23() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty V23() set
[:[:REAL,REAL:],REAL:] is non empty V23() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is ext-real positive non empty natural V14() real V16() V17() V18() V19() V20() V21() Element of NAT
[:2,2:] is non empty V23() set
[:[:2,2:],REAL:] is non empty V23() set
bool [:[:2,2:],REAL:] is non empty set
COMPLEX is non empty V16() V22() V43() set
{} is empty V16() V17() V18() V19() V20() V21() V22() V23() V24() V25() set
0 is ext-real empty natural V14() real V16() V17() V18() V19() V20() V21() V22() V23() V24() V25() Element of NAT
real_dist is V23() V26([:REAL,REAL:]) V27( REAL ) V28() V37([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
sqrt 0 is ext-real V14() real Element of REAL
F₃() is non empty set
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is non empty V23() set
[:[:F₁(),F₂():],[:F₁(),F₂():]:] is non empty V23() set
[:[:[:F₁(),F₂():],[:F₁(),F₂():]:],F₃():] is non empty V23() set
bool [:[:[:F₁(),F₂():],[:F₁(),F₂():]:],F₃():] is non empty set
x is V23() V26([:[:F₁(),F₂():],[:F₁(),F₂():]:]) V27(F₃()) V28() V37([:[:F₁(),F₂():],[:F₁(),F₂():]:],F₃()) Element of bool [:[:[:F₁(),F₂():],[:F₁(),F₂():]:],F₃():]
y is Element of F₁()
z is Element of F₁()
x9 is Element of F₂()
[y,x9] is Element of [:F₁(),F₂():]
y9 is Element of F₂()
[z,y9] is Element of [:F₁(),F₂():]
F₄(y,z,x9,y9) is Element of F₃()
z9 is Element of [:F₁(),F₂():]
y1 is Element of [:F₁(),F₂():]
x . (z9,y1) is Element of F₃()
y1 `1 is Element of F<sub>1</sub>()
y1 `2 is Element of F₂()
[(y1 `1),(y1 `2)] is Element of [:F₁(),F₂():]
z9 `1 is Element of F<sub>1</sub>()
z9 `2 is Element of F₂()
[(z9 `1),(z9 `2)] is Element of [:F₁(),F₂():]
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
x9 is Element of the carrier of x
y9 is Element of the carrier of x
dist (x9,y9) is ext-real V14() real Element of REAL
z9 is Element of the carrier of y
[x9,z9] is Element of [: the carrier of x, the carrier of y:]
y1 is Element of the carrier of y
[y9,y1] is Element of [: the carrier of x, the carrier of y:]
dist (z9,y1) is ext-real V14() real Element of REAL
(dist (x9,y9)) + (dist (z9,y1)) is ext-real V14() real Element of REAL
y2 is Element of [: the carrier of x, the carrier of y:]
y3 is Element of [: the carrier of x, the carrier of y:]
z . (y2,y3) is ext-real V14() real Element of REAL
z is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
x9 is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
y9 is Element of [: the carrier of x, the carrier of y:]
z9 is Element of [: the carrier of x, the carrier of y:]
z . (y9,z9) is ext-real V14() real Element of REAL
x9 . (y9,z9) is ext-real V14() real Element of REAL
y1 is Element of the carrier of x
y2 is Element of the carrier of y
[y1,y2] is Element of [: the carrier of x, the carrier of y:]
y3 is Element of the carrier of x
z1 is Element of the carrier of y
[y3,z1] is Element of [: the carrier of x, the carrier of y:]
dist (y1,y3) is ext-real V14() real Element of REAL
dist (y2,z1) is ext-real V14() real Element of REAL
(dist (y1,y3)) + (dist (y2,z1)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is Element of [: the carrier of x, the carrier of y:]
x9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,x9) is ext-real V14() real Element of REAL
z `1 is Element of the carrier of x
x9 `1 is Element of the carrier of x
z `2 is Element of the carrier of y
x9 `2 is Element of the carrier of y
y9 is Element of the carrier of x
y1 is Element of the carrier of y
[y9,y1] is Element of [: the carrier of x, the carrier of y:]
z9 is Element of the carrier of x
y2 is Element of the carrier of y
[z9,y2] is Element of [: the carrier of x, the carrier of y:]
dist (y9,z9) is ext-real V14() real Element of REAL
dist (y1,y2) is ext-real V14() real Element of REAL
(dist (y9,z9)) + (dist (y1,y2)) is ext-real V14() real Element of REAL
dist (y1,y2) is ext-real V14() real Element of REAL
dist (y9,z9) is ext-real V14() real Element of REAL
(dist (y9,z9)) + (dist (y1,y2)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is Element of [: the carrier of x, the carrier of y:]
x9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,x9) is ext-real V14() real Element of REAL
(x,y) . (x9,z) is ext-real V14() real Element of REAL
z `1 is Element of the carrier of x
x9 `1 is Element of the carrier of x
z `2 is Element of the carrier of y
x9 `2 is Element of the carrier of y
y9 is Element of the carrier of x
y1 is Element of the carrier of y
[y9,y1] is Element of [: the carrier of x, the carrier of y:]
z9 is Element of the carrier of x
y2 is Element of the carrier of y
[z9,y2] is Element of [: the carrier of x, the carrier of y:]
dist (z9,y9) is ext-real V14() real Element of REAL
dist (y1,y2) is ext-real V14() real Element of REAL
(dist (z9,y9)) + (dist (y1,y2)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is Element of [: the carrier of x, the carrier of y:]
y9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,y9) is ext-real V14() real Element of REAL
x9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,x9) is ext-real V14() real Element of REAL
(x,y) . (x9,y9) is ext-real V14() real Element of REAL
((x,y) . (z,x9)) + ((x,y) . (x9,y9)) is ext-real V14() real Element of REAL
z `1 is Element of the carrier of x
x9 `1 is Element of the carrier of x
y9 `1 is Element of the carrier of x
z `2 is Element of the carrier of y
x9 `2 is Element of the carrier of y
y9 `2 is Element of the carrier of y
y1 is Element of the carrier of x
z1 is Element of the carrier of y
[y1,z1] is Element of [: the carrier of x, the carrier of y:]
z2 is Element of the carrier of y
dist (z1,z2) is ext-real V14() real Element of REAL
y3 is Element of the carrier of y
dist (y3,z1) is ext-real V14() real Element of REAL
dist (y3,z2) is ext-real V14() real Element of REAL
y2 is Element of the carrier of x
dist (y1,y2) is ext-real V14() real Element of REAL
z9 is Element of the carrier of x
dist (z9,y1) is ext-real V14() real Element of REAL
dist (z9,y2) is ext-real V14() real Element of REAL
[y2,z2] is Element of [: the carrier of x, the carrier of y:]
[z9,y3] is Element of [: the carrier of x, the carrier of y:]
(dist (z9,y2)) + (dist (y3,z2)) is ext-real V14() real Element of REAL
(dist (z9,y1)) + (dist (y1,y2)) is ext-real V14() real Element of REAL
(dist (y3,z1)) + (dist (z1,z2)) is ext-real V14() real Element of REAL
((dist (z9,y1)) + (dist (y1,y2))) + ((dist (y3,z1)) + (dist (z1,z2))) is ext-real V14() real Element of REAL
(dist (z9,y1)) + (dist (y3,z1)) is ext-real V14() real Element of REAL
(dist (y1,y2)) + (dist (z1,z2)) is ext-real V14() real Element of REAL
((dist (z9,y1)) + (dist (y3,z1))) + ((dist (y1,y2)) + (dist (z1,z2))) is ext-real V14() real Element of REAL
((x,y) . (z,x9)) + ((dist (y1,y2)) + (dist (z1,z2))) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is Element of [: the carrier of x, the carrier of y:]
x9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,x9) is ext-real V14() real Element of REAL
x is non empty set
[:x,x:] is non empty V23() set
[:[:x,x:],REAL:] is non empty V23() set
bool [:[:x,x:],REAL:] is non empty set
y is V23() V26([:x,x:]) V27( REAL ) V28() V37([:x,x:], REAL ) Element of bool [:[:x,x:],REAL:]
MetrStruct(# x,y #) is strict MetrStruct
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #) is non empty strict MetrStruct
the carrier of MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #) is non empty set
x9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #)
y9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #)
dist (x9,y9) is ext-real V14() real Element of REAL
(x,y) . (x9,y9) is set
dist (y9,x9) is ext-real V14() real Element of REAL
(x,y) . (y9,x9) is set
z9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #)
dist (x9,z9) is ext-real V14() real Element of REAL
(x,y) . (x9,z9) is set
dist (y9,z9) is ext-real V14() real Element of REAL
(x,y) . (y9,z9) is set
(dist (x9,y9)) + (dist (y9,z9)) is ext-real V14() real Element of REAL
F₄() is non empty set
F₁() is non empty set
F₂() is non empty set
F₃() is non empty set
[:F₁(),F₂(),F₃():] is non empty set
[:[:F₁(),F₂(),F₃():],[:F₁(),F₂(),F₃():]:] is non empty V23() set
[:[:[:F₁(),F₂(),F₃():],[:F₁(),F₂(),F₃():]:],F₄():] is non empty V23() set
bool [:[:[:F₁(),F₂(),F₃():],[:F₁(),F₂(),F₃():]:],F₄():] is non empty set
x is V23() V26([:[:F₁(),F₂(),F₃():],[:F₁(),F₂(),F₃():]:]) V27(F₄()) V28() V37([:[:F₁(),F₂(),F₃():],[:F₁(),F₂(),F₃():]:],F₄()) Element of bool [:[:[:F₁(),F₂(),F₃():],[:F₁(),F₂(),F₃():]:],F₄():]
y is Element of F₁()
z is Element of F₁()
x9 is Element of F₂()
y9 is Element of F₂()
z9 is Element of F₃()
[y,x9,z9] is V35() Element of [:F₁(),F₂(),F₃():]
y1 is Element of F₃()
[z,y9,y1] is V35() Element of [:F₁(),F₂(),F₃():]
F₅(y,z,x9,y9,z9,y1) is Element of F₄()
y2 is V35() Element of [:F₁(),F₂(),F₃():]
y3 is V35() Element of [:F₁(),F₂(),F₃():]
x . (y2,y3) is Element of F₄()
y3 `1_3 is Element of F<sub>1</sub>()
y3 `2_3 is Element of F₂()
y3 `3_3 is Element of F<sub>3</sub>()
[(y3 `1_3),(y3 `2_3),(y3 `3_3)] is V35() Element of [:F₁(),F₂(),F₃():]
y2 `1_3 is Element of F<sub>1</sub>()
y2 `2_3 is Element of F₂()
y2 `3_3 is Element of F<sub>3</sub>()
[(y2 `1_3),(y2 `2_3),(y2 `3_3)] is V35() Element of [:F₁(),F₂(),F₃():]
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
y9 is Element of the carrier of x
z9 is Element of the carrier of x
dist (y9,z9) is ext-real V14() real Element of REAL
y1 is Element of the carrier of y
y2 is Element of the carrier of y
dist (y1,y2) is ext-real V14() real Element of REAL
(dist (y9,z9)) + (dist (y1,y2)) is ext-real V14() real Element of REAL
y3 is Element of the carrier of z
[y9,y1,y3] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
z1 is Element of the carrier of z
[z9,y2,z1] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
dist (y3,z1) is ext-real V14() real Element of REAL
((dist (y9,z9)) + (dist (y1,y2))) + (dist (y3,z1)) is ext-real V14() real Element of REAL
z2 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
z3 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
x9 . (z2,z3) is ext-real V14() real Element of REAL
x9 is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
y9 is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
z9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y1 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
x9 . (z9,y1) is ext-real V14() real Element of REAL
y9 . (z9,y1) is ext-real V14() real Element of REAL
y2 is Element of the carrier of x
y3 is Element of the carrier of y
z1 is Element of the carrier of z
[y2,y3,z1] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
z2 is Element of the carrier of x
z3 is Element of the carrier of y
d9 is Element of the carrier of z
[z2,z3,d9] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
dist (y2,z2) is ext-real V14() real Element of REAL
dist (y3,z3) is ext-real V14() real Element of REAL
(dist (y2,z2)) + (dist (y3,z3)) is ext-real V14() real Element of REAL
dist (z1,d9) is ext-real V14() real Element of REAL
((dist (y2,z2)) + (dist (y3,z3))) + (dist (z1,d9)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,y9) is ext-real V14() real Element of REAL
x9 `1_3 is Element of the carrier of x
y9 `1_3 is Element of the carrier of x
x9 `2_3 is Element of the carrier of y
y9 `2_3 is Element of the carrier of y
x9 `3_3 is Element of the carrier of z
y9 `3_3 is Element of the carrier of z
z9 is Element of the carrier of x
y2 is Element of the carrier of y
z1 is Element of the carrier of z
[z9,y2,z1] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y1 is Element of the carrier of x
y3 is Element of the carrier of y
z2 is Element of the carrier of z
[y1,y3,z2] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
dist (z1,z2) is ext-real V14() real Element of REAL
dist (y2,y3) is ext-real V14() real Element of REAL
dist (z9,y1) is ext-real V14() real Element of REAL
(dist (z9,y1)) + (dist (y2,y3)) is ext-real V14() real Element of REAL
((dist (z9,y1)) + (dist (y2,y3))) + (dist (z1,z2)) is ext-real V14() real Element of REAL
0 + 0 is ext-real V14() real Element of REAL
dist (z9,y1) is ext-real V14() real Element of REAL
dist (y2,y3) is ext-real V14() real Element of REAL
(dist (z9,y1)) + (dist (y2,y3)) is ext-real V14() real Element of REAL
dist (z1,z2) is ext-real V14() real Element of REAL
((dist (z9,y1)) + (dist (y2,y3))) + (dist (z1,z2)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,y9) is ext-real V14() real Element of REAL
(x,y,z) . (y9,x9) is ext-real V14() real Element of REAL
x9 `1_3 is Element of the carrier of x
y9 `1_3 is Element of the carrier of x
x9 `2_3 is Element of the carrier of y
y9 `2_3 is Element of the carrier of y
x9 `3_3 is Element of the carrier of z
y9 `3_3 is Element of the carrier of z
z9 is Element of the carrier of x
y2 is Element of the carrier of y
z1 is Element of the carrier of z
[z9,y2,z1] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y1 is Element of the carrier of x
y3 is Element of the carrier of y
z2 is Element of the carrier of z
[y1,y3,z2] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
dist (y1,z9) is ext-real V14() real Element of REAL
dist (y3,y2) is ext-real V14() real Element of REAL
(dist (y1,z9)) + (dist (y3,y2)) is ext-real V14() real Element of REAL
dist (z2,z1) is ext-real V14() real Element of REAL
((dist (y1,z9)) + (dist (y3,y2))) + (dist (z2,z1)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
z9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,z9) is ext-real V14() real Element of REAL
y9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,y9) is ext-real V14() real Element of REAL
(x,y,z) . (y9,z9) is ext-real V14() real Element of REAL
((x,y,z) . (x9,y9)) + ((x,y,z) . (y9,z9)) is ext-real V14() real Element of REAL
x9 `1_3 is Element of the carrier of x
y9 `1_3 is Element of the carrier of x
z9 `1_3 is Element of the carrier of x
x9 `2_3 is Element of the carrier of y
y9 `2_3 is Element of the carrier of y
z9 `2_3 is Element of the carrier of y
x9 `3_3 is Element of the carrier of z
y9 `3_3 is Element of the carrier of z
z9 `3_3 is Element of the carrier of z
y1 is Element of the carrier of x
z1 is Element of the carrier of y
d9 is Element of the carrier of z
[y1,z1,d9] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
z3 is Element of the carrier of y
dist (z1,z3) is ext-real V14() real Element of REAL
z2 is Element of the carrier of y
dist (z1,z2) is ext-real V14() real Element of REAL
dist (z2,z3) is ext-real V14() real Element of REAL
y3 is Element of the carrier of x
d6 is Element of the carrier of z
[y3,z3,d6] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
dist (d9,d6) is ext-real V14() real Element of REAL
d5 is Element of the carrier of z
dist (d9,d5) is ext-real V14() real Element of REAL
dist (d5,d6) is ext-real V14() real Element of REAL
dist (y1,y3) is ext-real V14() real Element of REAL
y2 is Element of the carrier of x
dist (y1,y2) is ext-real V14() real Element of REAL
dist (y2,y3) is ext-real V14() real Element of REAL
[y2,z2,d5] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(dist (y1,y3)) + (dist (z1,z3)) is ext-real V14() real Element of REAL
(dist (y1,y2)) + (dist (y2,y3)) is ext-real V14() real Element of REAL
(dist (z1,z2)) + (dist (z2,z3)) is ext-real V14() real Element of REAL
((dist (y1,y2)) + (dist (y2,y3))) + ((dist (z1,z2)) + (dist (z2,z3))) is ext-real V14() real Element of REAL
(dist (d9,d5)) + (dist (d5,d6)) is ext-real V14() real Element of REAL
((dist (y1,y3)) + (dist (z1,z3))) + (dist (d9,d6)) is ext-real V14() real Element of REAL
(((dist (y1,y2)) + (dist (y2,y3))) + ((dist (z1,z2)) + (dist (z2,z3)))) + ((dist (d9,d5)) + (dist (d5,d6))) is ext-real V14() real Element of REAL
(dist (y1,y2)) + (dist (z1,z2)) is ext-real V14() real Element of REAL
((dist (y1,y2)) + (dist (z1,z2))) + (dist (d9,d5)) is ext-real V14() real Element of REAL
(dist (y2,y3)) + (dist (z2,z3)) is ext-real V14() real Element of REAL
((dist (y2,y3)) + (dist (z2,z3))) + (dist (d5,d6)) is ext-real V14() real Element of REAL
(((dist (y1,y2)) + (dist (z1,z2))) + (dist (d9,d5))) + (((dist (y2,y3)) + (dist (z2,z3))) + (dist (d5,d6))) is ext-real V14() real Element of REAL
((x,y,z) . (x9,y9)) + (((dist (y2,y3)) + (dist (z2,z3))) + (dist (d5,d6))) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #) is non empty strict MetrStruct
the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #) is non empty set
y9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #)
z9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #)
dist (y9,z9) is ext-real V14() real Element of REAL
(x,y,z) . (y9,z9) is set
dist (z9,y9) is ext-real V14() real Element of REAL
(x,y,z) . (z9,y9) is set
y1 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #)
dist (y9,y1) is ext-real V14() real Element of REAL
(x,y,z) . (y9,y1) is set
dist (z9,y1) is ext-real V14() real Element of REAL
(x,y,z) . (z9,y1) is set
(dist (y9,z9)) + (dist (z9,y1)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,y9) is ext-real V14() real Element of REAL
F<sub>5</sub>() is non empty set
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty set
F<sub>3</sub>() is non empty set
F<sub>4</sub>() is non empty set
[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():] is non empty set
[:[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():],[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]:] is non empty V23() set
[:[:[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():],[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]:],F<sub>5</sub>():] is non empty V23() set
bool [:[:[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():],[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]:],F<sub>5</sub>():] is non empty set
x is V23() V26([:[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():],[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]:]) V27(F<sub>5</sub>()) V28() V37([:[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():],[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]:],F<sub>5</sub>()) Element of bool [:[:[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():],[:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]:],F<sub>5</sub>():]
y is Element of F<sub>1</sub>()
z is Element of F<sub>1</sub>()
x9 is Element of F<sub>2</sub>()
y9 is Element of F<sub>2</sub>()
z9 is Element of F<sub>3</sub>()
y1 is Element of F<sub>3</sub>()
y2 is Element of F<sub>4</sub>()
[y,x9,z9,y2] is V36() Element of [:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]
y3 is Element of F<sub>4</sub>()
[z,y9,y1,y3] is V36() Element of [:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]
F<sub>6</sub>(y,z,x9,y9,z9,y1,y2,y3) is Element of F<sub>5</sub>()
z1 is V36() Element of [:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]
z2 is V36() Element of [:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]
x . (z1,z2) is Element of F<sub>5</sub>()
z2 `1_4 is Element of F₁()
z2 `2_4 is Element of F<sub>2</sub>()
z2 `3_4 is Element of F₃()
z2 `4_4 is Element of F<sub>4</sub>()
[(z2 `1_4),(z2 `2_4),(z2 `3_4),(z2 `4_4)] is V36() Element of [:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]
z1 `1_4 is Element of F₁()
z1 `2_4 is Element of F<sub>2</sub>()
z1 `3_4 is Element of F₃()
z1 `4_4 is Element of F<sub>4</sub>()
[(z1 `1_4),(z1 `2_4),(z1 `3_4),(z1 `4_4)] is V36() Element of [:F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>():]
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
x9 is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x9 is non empty set
[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:] is non empty set
[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty set
y9 is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:]
z9 is Element of the carrier of x
y1 is Element of the carrier of x
dist (z9,y1) is ext-real V14() real Element of REAL
y2 is Element of the carrier of y
y3 is Element of the carrier of y
dist (y2,y3) is ext-real V14() real Element of REAL
(dist (z9,y1)) + (dist (y2,y3)) is ext-real V14() real Element of REAL
z1 is Element of the carrier of z
z2 is Element of the carrier of z
dist (z1,z2) is ext-real V14() real Element of REAL
z3 is Element of the carrier of x9
[z9,y2,z1,z3] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
d9 is Element of the carrier of x9
[y1,y3,z2,d9] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
dist (z3,d9) is ext-real V14() real Element of REAL
(dist (z1,z2)) + (dist (z3,d9)) is ext-real V14() real Element of REAL
((dist (z9,y1)) + (dist (y2,y3))) + ((dist (z1,z2)) + (dist (z3,d9))) is ext-real V14() real Element of REAL
d5 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
d6 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
y9 . (d5,d6) is ext-real V14() real Element of REAL
y9 is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:]
z9 is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:]
y1 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
y2 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
y9 . (y1,y2) is ext-real V14() real Element of REAL
z9 . (y1,y2) is ext-real V14() real Element of REAL
y3 is Element of the carrier of x
z1 is Element of the carrier of y
z2 is Element of the carrier of z
z3 is Element of the carrier of x9
[y3,z1,z2,z3] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
d9 is Element of the carrier of x
d5 is Element of the carrier of y
d6 is Element of the carrier of z
d1 is Element of the carrier of x9
[d9,d5,d6,d1] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
dist (y3,d9) is ext-real V14() real Element of REAL
dist (z1,d5) is ext-real V14() real Element of REAL
(dist (y3,d9)) + (dist (z1,d5)) is ext-real V14() real Element of REAL
dist (z2,d6) is ext-real V14() real Element of REAL
dist (z3,d1) is ext-real V14() real Element of REAL
(dist (z2,d6)) + (dist (z3,d1)) is ext-real V14() real Element of REAL
((dist (y3,d9)) + (dist (z1,d5))) + ((dist (z2,d6)) + (dist (z3,d1))) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
x9 is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x9 is non empty set
[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:] is non empty set
(x,y,z,x9) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty set
y9 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
z9 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
(x,y,z,x9) . (y9,z9) is ext-real V14() real Element of REAL
y9 `1_4 is Element of the carrier of x
z9 `1_4 is Element of the carrier of x
y9 `2_4 is Element of the carrier of y
z9 `2_4 is Element of the carrier of y
y9 `3_4 is Element of the carrier of z
z9 `3_4 is Element of the carrier of z
y9 `4_4 is Element of the carrier of x9
z9 `4_4 is Element of the carrier of x9
y1 is Element of the carrier of x
y3 is Element of the carrier of y
z2 is Element of the carrier of z
d9 is Element of the carrier of x9
[y1,y3,z2,d9] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
y2 is Element of the carrier of x
z1 is Element of the carrier of y
z3 is Element of the carrier of z
d5 is Element of the carrier of x9
[y2,z1,z3,d5] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
dist (y1,y2) is ext-real V14() real Element of REAL
dist (y3,z1) is ext-real V14() real Element of REAL
dist (z2,z3) is ext-real V14() real Element of REAL
dist (d9,d5) is ext-real V14() real Element of REAL
(dist (y1,y2)) + (dist (y3,z1)) is ext-real V14() real Element of REAL
(dist (z2,z3)) + (dist (d9,d5)) is ext-real V14() real Element of REAL
0 + 0 is ext-real V14() real Element of REAL
((dist (y1,y2)) + (dist (y3,z1))) + ((dist (z2,z3)) + (dist (d9,d5))) is ext-real V14() real Element of REAL
dist (y3,z1) is ext-real V14() real Element of REAL
dist (z2,z3) is ext-real V14() real Element of REAL
dist (d9,d5) is ext-real V14() real Element of REAL
dist (y1,y2) is ext-real V14() real Element of REAL
(dist (y1,y2)) + (dist (y3,z1)) is ext-real V14() real Element of REAL
(dist (z2,z3)) + (dist (d9,d5)) is ext-real V14() real Element of REAL
((dist (y1,y2)) + (dist (y3,z1))) + ((dist (z2,z3)) + (dist (d9,d5))) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
x9 is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x9 is non empty set
[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:] is non empty set
(x,y,z,x9) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty set
y9 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
z9 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
(x,y,z,x9) . (y9,z9) is ext-real V14() real Element of REAL
(x,y,z,x9) . (z9,y9) is ext-real V14() real Element of REAL
y9 `1_4 is Element of the carrier of x
z9 `1_4 is Element of the carrier of x
y9 `2_4 is Element of the carrier of y
z9 `2_4 is Element of the carrier of y
y9 `3_4 is Element of the carrier of z
z9 `3_4 is Element of the carrier of z
y9 `4_4 is Element of the carrier of x9
z9 `4_4 is Element of the carrier of x9
y1 is Element of the carrier of x
y3 is Element of the carrier of y
z2 is Element of the carrier of z
d9 is Element of the carrier of x9
[y1,y3,z2,d9] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
y2 is Element of the carrier of x
z1 is Element of the carrier of y
z3 is Element of the carrier of z
d5 is Element of the carrier of x9
[y2,z1,z3,d5] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
dist (y2,y1) is ext-real V14() real Element of REAL
dist (z1,y3) is ext-real V14() real Element of REAL
(dist (y2,y1)) + (dist (z1,y3)) is ext-real V14() real Element of REAL
dist (z3,z2) is ext-real V14() real Element of REAL
dist (d9,d5) is ext-real V14() real Element of REAL
(dist (z3,z2)) + (dist (d9,d5)) is ext-real V14() real Element of REAL
((dist (y2,y1)) + (dist (z1,y3))) + ((dist (z3,z2)) + (dist (d9,d5))) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
x9 is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x9 is non empty set
[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:] is non empty set
(x,y,z,x9) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty set
y9 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
y1 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
(x,y,z,x9) . (y9,y1) is ext-real V14() real Element of REAL
z9 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
(x,y,z,x9) . (y9,z9) is ext-real V14() real Element of REAL
(x,y,z,x9) . (z9,y1) is ext-real V14() real Element of REAL
((x,y,z,x9) . (y9,z9)) + ((x,y,z,x9) . (z9,y1)) is ext-real V14() real Element of REAL
y9 `1_4 is Element of the carrier of x
z9 `1_4 is Element of the carrier of x
y1 `1_4 is Element of the carrier of x
y9 `2_4 is Element of the carrier of y
z9 `2_4 is Element of the carrier of y
y1 `2_4 is Element of the carrier of y
y9 `3_4 is Element of the carrier of z
z9 `3_4 is Element of the carrier of z
y1 `3_4 is Element of the carrier of z
y9 `4_4 is Element of the carrier of x9
z9 `4_4 is Element of the carrier of x9
y1 `4_4 is Element of the carrier of x9
y2 is Element of the carrier of x
z2 is Element of the carrier of y
d5 is Element of the carrier of z
d2 is Element of the carrier of x9
[y2,z2,d5,d2] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
d1 is Element of the carrier of z
dist (d5,d1) is ext-real V14() real Element of REAL
d6 is Element of the carrier of z
dist (d5,d6) is ext-real V14() real Element of REAL
dist (d6,d1) is ext-real V14() real Element of REAL
z1 is Element of the carrier of x
dist (y2,z1) is ext-real V14() real Element of REAL
y3 is Element of the carrier of x
dist (y2,y3) is ext-real V14() real Element of REAL
dist (y3,z1) is ext-real V14() real Element of REAL
z3 is Element of the carrier of y
d7 is Element of the carrier of x9
[y3,z3,d6,d7] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
d8 is Element of the carrier of x9
dist (d2,d8) is ext-real V14() real Element of REAL
dist (d2,d7) is ext-real V14() real Element of REAL
dist (d7,d8) is ext-real V14() real Element of REAL
d9 is Element of the carrier of y
dist (z2,d9) is ext-real V14() real Element of REAL
dist (z2,z3) is ext-real V14() real Element of REAL
dist (z3,d9) is ext-real V14() real Element of REAL
[z1,d9,d1,d8] is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
(dist (d5,d1)) + (dist (d2,d8)) is ext-real V14() real Element of REAL
(dist (y2,z1)) + (dist (z2,d9)) is ext-real V14() real Element of REAL
(dist (d5,d6)) + (dist (d6,d1)) is ext-real V14() real Element of REAL
(dist (d2,d7)) + (dist (d7,d8)) is ext-real V14() real Element of REAL
((dist (d5,d6)) + (dist (d6,d1))) + ((dist (d2,d7)) + (dist (d7,d8))) is ext-real V14() real Element of REAL
(dist (y2,y3)) + (dist (y3,z1)) is ext-real V14() real Element of REAL
(dist (z2,z3)) + (dist (z3,d9)) is ext-real V14() real Element of REAL
((dist (y2,y3)) + (dist (y3,z1))) + ((dist (z2,z3)) + (dist (z3,d9))) is ext-real V14() real Element of REAL
((dist (y2,z1)) + (dist (z2,d9))) + ((dist (d5,d1)) + (dist (d2,d8))) is ext-real V14() real Element of REAL
(((dist (y2,y3)) + (dist (y3,z1))) + ((dist (z2,z3)) + (dist (z3,d9)))) + (((dist (d5,d6)) + (dist (d6,d1))) + ((dist (d2,d7)) + (dist (d7,d8)))) is ext-real V14() real Element of REAL
(dist (y2,y3)) + (dist (z2,z3)) is ext-real V14() real Element of REAL
(dist (d5,d6)) + (dist (d2,d7)) is ext-real V14() real Element of REAL
((dist (y2,y3)) + (dist (z2,z3))) + ((dist (d5,d6)) + (dist (d2,d7))) is ext-real V14() real Element of REAL
(dist (y3,z1)) + (dist (z3,d9)) is ext-real V14() real Element of REAL
(dist (d6,d1)) + (dist (d7,d8)) is ext-real V14() real Element of REAL
((dist (y3,z1)) + (dist (z3,d9))) + ((dist (d6,d1)) + (dist (d7,d8))) is ext-real V14() real Element of REAL
(((dist (y2,y3)) + (dist (z2,z3))) + ((dist (d5,d6)) + (dist (d2,d7)))) + (((dist (y3,z1)) + (dist (z3,d9))) + ((dist (d6,d1)) + (dist (d7,d8)))) is ext-real V14() real Element of REAL
((x,y,z,x9) . (y9,z9)) + (((dist (y3,z1)) + (dist (z3,d9))) + ((dist (d6,d1)) + (dist (d7,d8)))) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
x9 is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x9 is non empty set
[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:] is non empty set
(x,y,z,x9) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty set
MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],(x,y,z,x9) #) is non empty strict MetrStruct
the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],(x,y,z,x9) #) is non empty set
z9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],(x,y,z,x9) #)
y1 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],(x,y,z,x9) #)
y2 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],(x,y,z,x9) #)
dist (z9,y1) is ext-real V14() real Element of REAL
y3 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
z1 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
(x,y,z,x9) . (y3,z1) is ext-real V14() real Element of REAL
dist (y1,z9) is ext-real V14() real Element of REAL
(x,y,z,x9) . (z1,y3) is ext-real V14() real Element of REAL
dist (z9,y2) is ext-real V14() real Element of REAL
z2 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
(x,y,z,x9) . (y3,z2) is ext-real V14() real Element of REAL
dist (y1,y2) is ext-real V14() real Element of REAL
(x,y,z,x9) . (z1,z2) is ext-real V14() real Element of REAL
(dist (z9,y1)) + (dist (y1,y2)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
x9 is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x9 is non empty set
[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:] is non empty set
(x,y,z,x9) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:],[: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]:],REAL:] is non empty set
y9 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
z9 is V36() Element of [: the carrier of x, the carrier of y, the carrier of z, the carrier of x9:]
(x,y,z,x9) . (y9,z9) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
x9 is Element of the carrier of x
y9 is Element of the carrier of x
dist (x9,y9) is ext-real V14() real Element of REAL
(dist (x9,y9)) ^2 is ext-real V14() real Element of REAL
(dist (x9,y9)) * (dist (x9,y9)) is ext-real V14() real set
z9 is Element of the carrier of y
[x9,z9] is Element of [: the carrier of x, the carrier of y:]
y1 is Element of the carrier of y
[y9,y1] is Element of [: the carrier of x, the carrier of y:]
dist (z9,y1) is ext-real V14() real Element of REAL
(dist (z9,y1)) ^2 is ext-real V14() real Element of REAL
(dist (z9,y1)) * (dist (z9,y1)) is ext-real V14() real set
((dist (x9,y9)) ^2) + ((dist (z9,y1)) ^2) is ext-real V14() real Element of REAL
sqrt (((dist (x9,y9)) ^2) + ((dist (z9,y1)) ^2)) is ext-real V14() real Element of REAL
y2 is Element of [: the carrier of x, the carrier of y:]
y3 is Element of [: the carrier of x, the carrier of y:]
z . (y2,y3) is ext-real V14() real Element of REAL
z is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
x9 is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
y9 is Element of [: the carrier of x, the carrier of y:]
z9 is Element of [: the carrier of x, the carrier of y:]
z . (y9,z9) is ext-real V14() real Element of REAL
x9 . (y9,z9) is ext-real V14() real Element of REAL
y1 is Element of the carrier of x
y2 is Element of the carrier of y
[y1,y2] is Element of [: the carrier of x, the carrier of y:]
y3 is Element of the carrier of x
z1 is Element of the carrier of y
[y3,z1] is Element of [: the carrier of x, the carrier of y:]
dist (y1,y3) is ext-real V14() real Element of REAL
(dist (y1,y3)) ^2 is ext-real V14() real Element of REAL
(dist (y1,y3)) * (dist (y1,y3)) is ext-real V14() real set
dist (y2,z1) is ext-real V14() real Element of REAL
(dist (y2,z1)) ^2 is ext-real V14() real Element of REAL
(dist (y2,z1)) * (dist (y2,z1)) is ext-real V14() real set
((dist (y1,y3)) ^2) + ((dist (y2,z1)) ^2) is ext-real V14() real Element of REAL
sqrt (((dist (y1,y3)) ^2) + ((dist (y2,z1)) ^2)) is ext-real V14() real Element of REAL
x is ext-real V14() real set
y is ext-real V14() real set
x + y is ext-real V14() real set
sqrt (x + y) is ext-real V14() real set
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is Element of [: the carrier of x, the carrier of y:]
x9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,x9) is ext-real V14() real Element of REAL
z `1 is Element of the carrier of x
x9 `1 is Element of the carrier of x
z `2 is Element of the carrier of y
x9 `2 is Element of the carrier of y
y9 is Element of the carrier of x
y1 is Element of the carrier of y
[y9,y1] is Element of [: the carrier of x, the carrier of y:]
z9 is Element of the carrier of x
y2 is Element of the carrier of y
[z9,y2] is Element of [: the carrier of x, the carrier of y:]
dist (y1,y2) is ext-real V14() real Element of REAL
dist (y9,z9) is ext-real V14() real Element of REAL
(dist (y9,z9)) ^2 is ext-real V14() real Element of REAL
(dist (y9,z9)) * (dist (y9,z9)) is ext-real V14() real set
(dist (y1,y2)) ^2 is ext-real V14() real Element of REAL
(dist (y1,y2)) * (dist (y1,y2)) is ext-real V14() real set
((dist (y9,z9)) ^2) + ((dist (y1,y2)) ^2) is ext-real V14() real Element of REAL
sqrt (((dist (y9,z9)) ^2) + ((dist (y1,y2)) ^2)) is ext-real V14() real Element of REAL
dist (y9,z9) is ext-real V14() real Element of REAL
(dist (y9,z9)) ^2 is ext-real V14() real Element of REAL
(dist (y9,z9)) * (dist (y9,z9)) is ext-real V14() real set
0 ^2 is ext-real V14() real Element of REAL
0 * 0 is ext-real V14() real set
dist (y1,y2) is ext-real V14() real Element of REAL
(dist (y1,y2)) ^2 is ext-real V14() real Element of REAL
(dist (y1,y2)) * (dist (y1,y2)) is ext-real V14() real set
((dist (y9,z9)) ^2) + ((dist (y1,y2)) ^2) is ext-real V14() real Element of REAL
sqrt (((dist (y9,z9)) ^2) + ((dist (y1,y2)) ^2)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is Element of [: the carrier of x, the carrier of y:]
x9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,x9) is ext-real V14() real Element of REAL
(x,y) . (x9,z) is ext-real V14() real Element of REAL
z `1 is Element of the carrier of x
x9 `1 is Element of the carrier of x
z `2 is Element of the carrier of y
x9 `2 is Element of the carrier of y
y9 is Element of the carrier of x
y1 is Element of the carrier of y
[y9,y1] is Element of [: the carrier of x, the carrier of y:]
z9 is Element of the carrier of x
y2 is Element of the carrier of y
[z9,y2] is Element of [: the carrier of x, the carrier of y:]
dist (z9,y9) is ext-real V14() real Element of REAL
(dist (z9,y9)) ^2 is ext-real V14() real Element of REAL
(dist (z9,y9)) * (dist (z9,y9)) is ext-real V14() real set
dist (y1,y2) is ext-real V14() real Element of REAL
(dist (y1,y2)) ^2 is ext-real V14() real Element of REAL
(dist (y1,y2)) * (dist (y1,y2)) is ext-real V14() real set
((dist (z9,y9)) ^2) + ((dist (y1,y2)) ^2) is ext-real V14() real Element of REAL
sqrt (((dist (z9,y9)) ^2) + ((dist (y1,y2)) ^2)) is ext-real V14() real Element of REAL
x is ext-real V14() real set
y is ext-real V14() real set
z is ext-real V14() real set
x9 is ext-real V14() real set
x + z is ext-real V14() real set
(x + z) ^2 is ext-real V14() real set
(x + z) * (x + z) is ext-real V14() real set
y + x9 is ext-real V14() real set
(y + x9) ^2 is ext-real V14() real set
(y + x9) * (y + x9) is ext-real V14() real set
((x + z) ^2) + ((y + x9) ^2) is ext-real V14() real set
sqrt (((x + z) ^2) + ((y + x9) ^2)) is ext-real V14() real set
x ^2 is ext-real V14() real set
x * x is ext-real V14() real set
y ^2 is ext-real V14() real set
y * y is ext-real V14() real set
(x ^2) + (y ^2) is ext-real V14() real set
sqrt ((x ^2) + (y ^2)) is ext-real V14() real set
z ^2 is ext-real V14() real set
z * z is ext-real V14() real set
x9 ^2 is ext-real V14() real set
x9 * x9 is ext-real V14() real set
(z ^2) + (x9 ^2) is ext-real V14() real set
sqrt ((z ^2) + (x9 ^2)) is ext-real V14() real set
(sqrt ((x ^2) + (y ^2))) + (sqrt ((z ^2) + (x9 ^2))) is ext-real V14() real set
x * z is ext-real V14() real set
x9 * y is ext-real V14() real set
0 + 0 is ext-real V14() real Element of REAL
(x * z) + (x9 * y) is ext-real V14() real set
x * x9 is ext-real V14() real set
z * y is ext-real V14() real set
(x * x9) - (z * y) is ext-real V14() real set
((x * x9) - (z * y)) ^2 is ext-real V14() real set
((x * x9) - (z * y)) * ((x * x9) - (z * y)) is ext-real V14() real set
(x ^2) * (x9 ^2) is ext-real V14() real set
(z ^2) * (y ^2) is ext-real V14() real set
((x ^2) * (x9 ^2)) + ((z ^2) * (y ^2)) is ext-real V14() real set
2 * (x * x9) is ext-real V14() real Element of REAL
(2 * (x * x9)) * (z * y) is ext-real V14() real Element of REAL
(((x ^2) * (x9 ^2)) + ((z ^2) * (y ^2))) - ((2 * (x * x9)) * (z * y)) is ext-real V14() real Element of REAL
0 + ((2 * (x * x9)) * (z * y)) is ext-real V14() real Element of REAL
(y ^2) * (x9 ^2) is ext-real V14() real set
((y ^2) * (x9 ^2)) + ((2 * (x * x9)) * (z * y)) is ext-real V14() real Element of REAL
(((x ^2) * (x9 ^2)) + ((z ^2) * (y ^2))) + ((y ^2) * (x9 ^2)) is ext-real V14() real set
(x ^2) * (z ^2) is ext-real V14() real set
((x ^2) * (z ^2)) + (((y ^2) * (x9 ^2)) + ((2 * (x * x9)) * (z * y))) is ext-real V14() real Element of REAL
((y ^2) * (x9 ^2)) + (((x ^2) * (x9 ^2)) + ((z ^2) * (y ^2))) is ext-real V14() real set
((x ^2) * (z ^2)) + (((y ^2) * (x9 ^2)) + (((x ^2) * (x9 ^2)) + ((z ^2) * (y ^2)))) is ext-real V14() real set
((x * z) + (x9 * y)) ^2 is ext-real V14() real set
((x * z) + (x9 * y)) * ((x * z) + (x9 * y)) is ext-real V14() real set
sqrt (((x * z) + (x9 * y)) ^2) is ext-real V14() real set
((x ^2) + (y ^2)) * ((z ^2) + (x9 ^2)) is ext-real V14() real set
sqrt (((x ^2) + (y ^2)) * ((z ^2) + (x9 ^2))) is ext-real V14() real set
2 * (sqrt (((x * z) + (x9 * y)) ^2)) is ext-real V14() real Element of REAL
2 * (sqrt (((x ^2) + (y ^2)) * ((z ^2) + (x9 ^2)))) is ext-real V14() real Element of REAL
(sqrt ((x ^2) + (y ^2))) * (sqrt ((z ^2) + (x9 ^2))) is ext-real V14() real set
2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((z ^2) + (x9 ^2)))) is ext-real V14() real Element of REAL
2 * ((x * z) + (x9 * y)) is ext-real V14() real Element of REAL
(x9 ^2) + (z ^2) is ext-real V14() real set
sqrt ((x9 ^2) + (z ^2)) is ext-real V14() real set
(sqrt ((x ^2) + (y ^2))) * (sqrt ((x9 ^2) + (z ^2))) is ext-real V14() real set
2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((x9 ^2) + (z ^2)))) is ext-real V14() real Element of REAL
(y ^2) + (2 * ((x * z) + (x9 * y))) is ext-real V14() real Element of REAL
(2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((x9 ^2) + (z ^2))))) + (y ^2) is ext-real V14() real Element of REAL
(x9 ^2) + ((y ^2) + (2 * ((x * z) + (x9 * y)))) is ext-real V14() real Element of REAL
(y ^2) + (2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((x9 ^2) + (z ^2))))) is ext-real V14() real Element of REAL
(x9 ^2) + ((y ^2) + (2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((x9 ^2) + (z ^2)))))) is ext-real V14() real Element of REAL
(z ^2) + ((x9 ^2) + ((y ^2) + (2 * ((x * z) + (x9 * y))))) is ext-real V14() real Element of REAL
((x9 ^2) + ((y ^2) + (2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((x9 ^2) + (z ^2))))))) + (z ^2) is ext-real V14() real Element of REAL
2 * (x9 * y) is ext-real V14() real Element of REAL
(y ^2) + (2 * (x9 * y)) is ext-real V14() real Element of REAL
2 * (x * z) is ext-real V14() real Element of REAL
((y ^2) + (2 * (x9 * y))) + (2 * (x * z)) is ext-real V14() real Element of REAL
(x9 ^2) + (((y ^2) + (2 * (x9 * y))) + (2 * (x * z))) is ext-real V14() real Element of REAL
(z ^2) + ((x9 ^2) + (((y ^2) + (2 * (x9 * y))) + (2 * (x * z)))) is ext-real V14() real Element of REAL
(x ^2) + ((z ^2) + ((x9 ^2) + (((y ^2) + (2 * (x9 * y))) + (2 * (x * z))))) is ext-real V14() real Element of REAL
(z ^2) + ((x9 ^2) + ((y ^2) + (2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((x9 ^2) + (z ^2))))))) is ext-real V14() real Element of REAL
(x ^2) + ((z ^2) + ((x9 ^2) + ((y ^2) + (2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((x9 ^2) + (z ^2)))))))) is ext-real V14() real Element of REAL
x9 + y is ext-real V14() real set
(x9 + y) ^2 is ext-real V14() real set
(x9 + y) * (x9 + y) is ext-real V14() real set
((x + z) ^2) + ((x9 + y) ^2) is ext-real V14() real set
((x ^2) + (y ^2)) + (2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((z ^2) + (x9 ^2))))) is ext-real V14() real Element of REAL
(((x ^2) + (y ^2)) + (2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((z ^2) + (x9 ^2)))))) + ((z ^2) + (x9 ^2)) is ext-real V14() real Element of REAL
(sqrt ((x ^2) + (y ^2))) ^2 is ext-real V14() real set
(sqrt ((x ^2) + (y ^2))) * (sqrt ((x ^2) + (y ^2))) is ext-real V14() real set
((sqrt ((x ^2) + (y ^2))) ^2) + (2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((z ^2) + (x9 ^2))))) is ext-real V14() real Element of REAL
(((sqrt ((x ^2) + (y ^2))) ^2) + (2 * ((sqrt ((x ^2) + (y ^2))) * (sqrt ((z ^2) + (x9 ^2)))))) + ((z ^2) + (x9 ^2)) is ext-real V14() real Element of REAL
2 * (sqrt ((x ^2) + (y ^2))) is ext-real V14() real Element of REAL
(2 * (sqrt ((x ^2) + (y ^2)))) * (sqrt ((z ^2) + (x9 ^2))) is ext-real V14() real Element of REAL
((sqrt ((x ^2) + (y ^2))) ^2) + ((2 * (sqrt ((x ^2) + (y ^2)))) * (sqrt ((z ^2) + (x9 ^2)))) is ext-real V14() real Element of REAL
(sqrt ((z ^2) + (x9 ^2))) ^2 is ext-real V14() real set
(sqrt ((z ^2) + (x9 ^2))) * (sqrt ((z ^2) + (x9 ^2))) is ext-real V14() real set
(((sqrt ((x ^2) + (y ^2))) ^2) + ((2 * (sqrt ((x ^2) + (y ^2)))) * (sqrt ((z ^2) + (x9 ^2))))) + ((sqrt ((z ^2) + (x9 ^2))) ^2) is ext-real V14() real Element of REAL
sqrt (((x + z) ^2) + ((x9 + y) ^2)) is ext-real V14() real set
((sqrt ((x ^2) + (y ^2))) + (sqrt ((z ^2) + (x9 ^2)))) ^2 is ext-real V14() real set
((sqrt ((x ^2) + (y ^2))) + (sqrt ((z ^2) + (x9 ^2)))) * ((sqrt ((x ^2) + (y ^2))) + (sqrt ((z ^2) + (x9 ^2)))) is ext-real V14() real set
sqrt (((sqrt ((x ^2) + (y ^2))) + (sqrt ((z ^2) + (x9 ^2)))) ^2) is ext-real V14() real set
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is Element of [: the carrier of x, the carrier of y:]
y9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,y9) is ext-real V14() real Element of REAL
x9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,x9) is ext-real V14() real Element of REAL
(x,y) . (x9,y9) is ext-real V14() real Element of REAL
((x,y) . (z,x9)) + ((x,y) . (x9,y9)) is ext-real V14() real Element of REAL
z `1 is Element of the carrier of x
x9 `1 is Element of the carrier of x
y9 `1 is Element of the carrier of x
z `2 is Element of the carrier of y
x9 `2 is Element of the carrier of y
y9 `2 is Element of the carrier of y
z9 is Element of the carrier of x
y3 is Element of the carrier of y
[z9,y3] is Element of [: the carrier of x, the carrier of y:]
z1 is Element of the carrier of y
dist (y3,z1) is ext-real V14() real Element of REAL
y1 is Element of the carrier of x
y2 is Element of the carrier of x
dist (y1,y2) is ext-real V14() real Element of REAL
dist (z9,y2) is ext-real V14() real Element of REAL
[y1,z1] is Element of [: the carrier of x, the carrier of y:]
z2 is Element of the carrier of y
dist (z1,z2) is ext-real V14() real Element of REAL
dist (y3,z2) is ext-real V14() real Element of REAL
dist (z9,y1) is ext-real V14() real Element of REAL
[y2,z2] is Element of [: the carrier of x, the carrier of y:]
(dist (z9,y2)) ^2 is ext-real V14() real Element of REAL
(dist (z9,y2)) * (dist (z9,y2)) is ext-real V14() real set
(dist (y3,z2)) ^2 is ext-real V14() real Element of REAL
(dist (y3,z2)) * (dist (y3,z2)) is ext-real V14() real set
0 + 0 is ext-real V14() real Element of REAL
((dist (z9,y2)) ^2) + ((dist (y3,z2)) ^2) is ext-real V14() real Element of REAL
(dist (y3,z1)) + (dist (z1,z2)) is ext-real V14() real Element of REAL
((dist (y3,z1)) + (dist (z1,z2))) ^2 is ext-real V14() real Element of REAL
((dist (y3,z1)) + (dist (z1,z2))) * ((dist (y3,z1)) + (dist (z1,z2))) is ext-real V14() real set
(dist (z9,y1)) + (dist (y1,y2)) is ext-real V14() real Element of REAL
((dist (z9,y1)) + (dist (y1,y2))) ^2 is ext-real V14() real Element of REAL
((dist (z9,y1)) + (dist (y1,y2))) * ((dist (z9,y1)) + (dist (y1,y2))) is ext-real V14() real set
(((dist (z9,y1)) + (dist (y1,y2))) ^2) + (((dist (y3,z1)) + (dist (z1,z2))) ^2) is ext-real V14() real Element of REAL
sqrt (((dist (z9,y2)) ^2) + ((dist (y3,z2)) ^2)) is ext-real V14() real Element of REAL
sqrt ((((dist (z9,y1)) + (dist (y1,y2))) ^2) + (((dist (y3,z1)) + (dist (z1,z2))) ^2)) is ext-real V14() real Element of REAL
(dist (z9,y1)) ^2 is ext-real V14() real Element of REAL
(dist (z9,y1)) * (dist (z9,y1)) is ext-real V14() real set
(dist (y3,z1)) ^2 is ext-real V14() real Element of REAL
(dist (y3,z1)) * (dist (y3,z1)) is ext-real V14() real set
((dist (z9,y1)) ^2) + ((dist (y3,z1)) ^2) is ext-real V14() real Element of REAL
sqrt (((dist (z9,y1)) ^2) + ((dist (y3,z1)) ^2)) is ext-real V14() real Element of REAL
(dist (y1,y2)) ^2 is ext-real V14() real Element of REAL
(dist (y1,y2)) * (dist (y1,y2)) is ext-real V14() real set
(dist (z1,z2)) ^2 is ext-real V14() real Element of REAL
(dist (z1,z2)) * (dist (z1,z2)) is ext-real V14() real set
((dist (y1,y2)) ^2) + ((dist (z1,z2)) ^2) is ext-real V14() real Element of REAL
sqrt (((dist (y1,y2)) ^2) + ((dist (z1,z2)) ^2)) is ext-real V14() real Element of REAL
(sqrt (((dist (z9,y1)) ^2) + ((dist (y3,z1)) ^2))) + (sqrt (((dist (y1,y2)) ^2) + ((dist (z1,z2)) ^2))) is ext-real V14() real Element of REAL
((x,y) . (z,x9)) + (sqrt (((dist (y1,y2)) ^2) + ((dist (z1,z2)) ^2))) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
z is Element of [: the carrier of x, the carrier of y:]
x9 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z,x9) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
[: the carrier of x, the carrier of y:] is non empty V23() set
(x,y) is V23() V26([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:]
[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y:],[: the carrier of x, the carrier of y:]:],REAL:] is non empty set
MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #) is non empty strict MetrStruct
the carrier of MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #) is non empty set
z is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #)
x9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #)
y9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y:],(x,y) #)
dist (z,x9) is ext-real V14() real Element of REAL
z9 is Element of [: the carrier of x, the carrier of y:]
y1 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z9,y1) is ext-real V14() real Element of REAL
dist (x9,z) is ext-real V14() real Element of REAL
(x,y) . (y1,z9) is ext-real V14() real Element of REAL
dist (z,y9) is ext-real V14() real Element of REAL
y2 is Element of [: the carrier of x, the carrier of y:]
(x,y) . (z9,y2) is ext-real V14() real Element of REAL
dist (x9,y9) is ext-real V14() real Element of REAL
(x,y) . (y1,y2) is ext-real V14() real Element of REAL
(dist (z,x9)) + (dist (x9,y9)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
y9 is Element of the carrier of x
z9 is Element of the carrier of x
dist (y9,z9) is ext-real V14() real Element of REAL
(dist (y9,z9)) ^2 is ext-real V14() real Element of REAL
(dist (y9,z9)) * (dist (y9,z9)) is ext-real V14() real set
y1 is Element of the carrier of y
y2 is Element of the carrier of y
dist (y1,y2) is ext-real V14() real Element of REAL
(dist (y1,y2)) ^2 is ext-real V14() real Element of REAL
(dist (y1,y2)) * (dist (y1,y2)) is ext-real V14() real set
((dist (y9,z9)) ^2) + ((dist (y1,y2)) ^2) is ext-real V14() real Element of REAL
y3 is Element of the carrier of z
[y9,y1,y3] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
z1 is Element of the carrier of z
[z9,y2,z1] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
dist (y3,z1) is ext-real V14() real Element of REAL
(dist (y3,z1)) ^2 is ext-real V14() real Element of REAL
(dist (y3,z1)) * (dist (y3,z1)) is ext-real V14() real set
(((dist (y9,z9)) ^2) + ((dist (y1,y2)) ^2)) + ((dist (y3,z1)) ^2) is ext-real V14() real Element of REAL
sqrt ((((dist (y9,z9)) ^2) + ((dist (y1,y2)) ^2)) + ((dist (y3,z1)) ^2)) is ext-real V14() real Element of REAL
z2 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
z3 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
x9 . (z2,z3) is ext-real V14() real Element of REAL
x9 is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
y9 is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
z9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y1 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
x9 . (z9,y1) is ext-real V14() real Element of REAL
y9 . (z9,y1) is ext-real V14() real Element of REAL
y2 is Element of the carrier of x
y3 is Element of the carrier of y
z1 is Element of the carrier of z
[y2,y3,z1] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
z2 is Element of the carrier of x
z3 is Element of the carrier of y
d9 is Element of the carrier of z
[z2,z3,d9] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
dist (y2,z2) is ext-real V14() real Element of REAL
(dist (y2,z2)) ^2 is ext-real V14() real Element of REAL
(dist (y2,z2)) * (dist (y2,z2)) is ext-real V14() real set
dist (y3,z3) is ext-real V14() real Element of REAL
(dist (y3,z3)) ^2 is ext-real V14() real Element of REAL
(dist (y3,z3)) * (dist (y3,z3)) is ext-real V14() real set
((dist (y2,z2)) ^2) + ((dist (y3,z3)) ^2) is ext-real V14() real Element of REAL
dist (z1,d9) is ext-real V14() real Element of REAL
(dist (z1,d9)) ^2 is ext-real V14() real Element of REAL
(dist (z1,d9)) * (dist (z1,d9)) is ext-real V14() real set
(((dist (y2,z2)) ^2) + ((dist (y3,z3)) ^2)) + ((dist (z1,d9)) ^2) is ext-real V14() real Element of REAL
sqrt ((((dist (y2,z2)) ^2) + ((dist (y3,z3)) ^2)) + ((dist (z1,d9)) ^2)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,y9) is ext-real V14() real Element of REAL
x9 `1_3 is Element of the carrier of x
y9 `1_3 is Element of the carrier of x
x9 `2_3 is Element of the carrier of y
y9 `2_3 is Element of the carrier of y
x9 `3_3 is Element of the carrier of z
y9 `3_3 is Element of the carrier of z
z9 is Element of the carrier of x
y2 is Element of the carrier of y
z1 is Element of the carrier of z
[z9,y2,z1] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y1 is Element of the carrier of x
y3 is Element of the carrier of y
z2 is Element of the carrier of z
[y1,y3,z2] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
dist (z1,z2) is ext-real V14() real Element of REAL
dist (y2,y3) is ext-real V14() real Element of REAL
dist (z9,y1) is ext-real V14() real Element of REAL
(dist (y2,y3)) ^2 is ext-real V14() real Element of REAL
(dist (y2,y3)) * (dist (y2,y3)) is ext-real V14() real set
(dist (z1,z2)) ^2 is ext-real V14() real Element of REAL
(dist (z1,z2)) * (dist (z1,z2)) is ext-real V14() real set
(dist (z9,y1)) ^2 is ext-real V14() real Element of REAL
(dist (z9,y1)) * (dist (z9,y1)) is ext-real V14() real set
((dist (z9,y1)) ^2) + ((dist (y2,y3)) ^2) is ext-real V14() real Element of REAL
(((dist (z9,y1)) ^2) + ((dist (y2,y3)) ^2)) + ((dist (z1,z2)) ^2) is ext-real V14() real Element of REAL
sqrt ((((dist (z9,y1)) ^2) + ((dist (y2,y3)) ^2)) + ((dist (z1,z2)) ^2)) is ext-real V14() real Element of REAL
((dist (y2,y3)) ^2) + ((dist (z1,z2)) ^2) is ext-real V14() real Element of REAL
((dist (z9,y1)) ^2) + (((dist (y2,y3)) ^2) + ((dist (z1,z2)) ^2)) is ext-real V14() real Element of REAL
sqrt (((dist (z9,y1)) ^2) + (((dist (y2,y3)) ^2) + ((dist (z1,z2)) ^2))) is ext-real V14() real Element of REAL
0 + 0 is ext-real V14() real Element of REAL
dist (z9,y1) is ext-real V14() real Element of REAL
(dist (z9,y1)) ^2 is ext-real V14() real Element of REAL
(dist (z9,y1)) * (dist (z9,y1)) is ext-real V14() real set
0 ^2 is ext-real V14() real Element of REAL
0 * 0 is ext-real V14() real set
dist (y2,y3) is ext-real V14() real Element of REAL
(dist (y2,y3)) ^2 is ext-real V14() real Element of REAL
(dist (y2,y3)) * (dist (y2,y3)) is ext-real V14() real set
((dist (z9,y1)) ^2) + ((dist (y2,y3)) ^2) is ext-real V14() real Element of REAL
dist (z1,z2) is ext-real V14() real Element of REAL
(dist (z1,z2)) ^2 is ext-real V14() real Element of REAL
(dist (z1,z2)) * (dist (z1,z2)) is ext-real V14() real set
(((dist (z9,y1)) ^2) + ((dist (y2,y3)) ^2)) + ((dist (z1,z2)) ^2) is ext-real V14() real Element of REAL
sqrt ((((dist (z9,y1)) ^2) + ((dist (y2,y3)) ^2)) + ((dist (z1,z2)) ^2)) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,y9) is ext-real V14() real Element of REAL
(x,y,z) . (y9,x9) is ext-real V14() real Element of REAL
x9 `1_3 is Element of the carrier of x
y9 `1_3 is Element of the carrier of x
x9 `2_3 is Element of the carrier of y
y9 `2_3 is Element of the carrier of y
x9 `3_3 is Element of the carrier of z
y9 `3_3 is Element of the carrier of z
z9 is Element of the carrier of x
y2 is Element of the carrier of y
z1 is Element of the carrier of z
[z9,y2,z1] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y1 is Element of the carrier of x
y3 is Element of the carrier of y
z2 is Element of the carrier of z
[y1,y3,z2] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
dist (y1,z9) is ext-real V14() real Element of REAL
(dist (y1,z9)) ^2 is ext-real V14() real Element of REAL
(dist (y1,z9)) * (dist (y1,z9)) is ext-real V14() real set
dist (y3,y2) is ext-real V14() real Element of REAL
(dist (y3,y2)) ^2 is ext-real V14() real Element of REAL
(dist (y3,y2)) * (dist (y3,y2)) is ext-real V14() real set
((dist (y1,z9)) ^2) + ((dist (y3,y2)) ^2) is ext-real V14() real Element of REAL
dist (z2,z1) is ext-real V14() real Element of REAL
(dist (z2,z1)) ^2 is ext-real V14() real Element of REAL
(dist (z2,z1)) * (dist (z2,z1)) is ext-real V14() real set
(((dist (y1,z9)) ^2) + ((dist (y3,y2)) ^2)) + ((dist (z2,z1)) ^2) is ext-real V14() real Element of REAL
sqrt ((((dist (y1,z9)) ^2) + ((dist (y3,y2)) ^2)) + ((dist (z2,z1)) ^2)) is ext-real V14() real Element of REAL
x is ext-real V14() real set
x9 is ext-real V14() real set
x * x9 is ext-real V14() real set
2 * (x * x9) is ext-real V14() real Element of REAL
z is ext-real V14() real set
y is ext-real V14() real set
z * y is ext-real V14() real set
(2 * (x * x9)) * (z * y) is ext-real V14() real Element of REAL
z9 is ext-real V14() real set
x * z9 is ext-real V14() real set
2 * (x * z9) is ext-real V14() real Element of REAL
y9 is ext-real V14() real set
y9 * z is ext-real V14() real set
(2 * (x * z9)) * (y9 * z) is ext-real V14() real Element of REAL
((2 * (x * x9)) * (z * y)) + ((2 * (x * z9)) * (y9 * z)) is ext-real V14() real Element of REAL
y * z9 is ext-real V14() real set
2 * (y * z9) is ext-real V14() real Element of REAL
y9 * x9 is ext-real V14() real set
(2 * (y * z9)) * (y9 * x9) is ext-real V14() real Element of REAL
(((2 * (x * x9)) * (z * y)) + ((2 * (x * z9)) * (y9 * z))) + ((2 * (y * z9)) * (y9 * x9)) is ext-real V14() real Element of REAL
(x * x9) ^2 is ext-real V14() real set
(x * x9) * (x * x9) is ext-real V14() real set
(z * y) ^2 is ext-real V14() real set
(z * y) * (z * y) is ext-real V14() real set
((x * x9) ^2) + ((z * y) ^2) is ext-real V14() real set
(x * z9) ^2 is ext-real V14() real set
(x * z9) * (x * z9) is ext-real V14() real set
(((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2) is ext-real V14() real set
(y9 * z) ^2 is ext-real V14() real set
(y9 * z) * (y9 * z) is ext-real V14() real set
((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2) is ext-real V14() real set
(y * z9) ^2 is ext-real V14() real set
(y * z9) * (y * z9) is ext-real V14() real set
(((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + ((y * z9) ^2) is ext-real V14() real set
(y9 * x9) ^2 is ext-real V14() real set
(y9 * x9) * (y9 * x9) is ext-real V14() real set
((((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + ((y * z9) ^2)) + ((y9 * x9) ^2) is ext-real V14() real set
(x * z9) - (y9 * z) is ext-real V14() real set
((x * z9) - (y9 * z)) ^2 is ext-real V14() real set
((x * z9) - (y9 * z)) * ((x * z9) - (y9 * z)) is ext-real V14() real set
(y * z9) - (y9 * x9) is ext-real V14() real set
((y * z9) - (y9 * x9)) ^2 is ext-real V14() real set
((y * z9) - (y9 * x9)) * ((y * z9) - (y9 * x9)) is ext-real V14() real set
(x * x9) - (z * y) is ext-real V14() real set
((x * x9) - (z * y)) ^2 is ext-real V14() real set
((x * x9) - (z * y)) * ((x * x9) - (z * y)) is ext-real V14() real set
0 + 0 is ext-real V14() real Element of REAL
(((x * z9) - (y9 * z)) ^2) + (((y * z9) - (y9 * x9)) ^2) is ext-real V14() real set
(((x * x9) - (z * y)) ^2) + ((((x * z9) - (y9 * z)) ^2) + (((y * z9) - (y9 * x9)) ^2)) is ext-real V14() real set
(((x * x9) ^2) + ((z * y) ^2)) + (((x * z9) - (y9 * z)) ^2) is ext-real V14() real set
((((x * x9) ^2) + ((z * y) ^2)) + (((x * z9) - (y9 * z)) ^2)) + (((y * z9) - (y9 * x9)) ^2) is ext-real V14() real set
(((((x * x9) ^2) + ((z * y) ^2)) + (((x * z9) - (y9 * z)) ^2)) + (((y * z9) - (y9 * x9)) ^2)) - ((2 * (x * x9)) * (z * y)) is ext-real V14() real Element of REAL
0 + ((2 * (x * x9)) * (z * y)) is ext-real V14() real Element of REAL
(((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + (((y * z9) - (y9 * x9)) ^2) is ext-real V14() real set
((((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + (((y * z9) - (y9 * x9)) ^2)) - ((2 * (x * z9)) * (y9 * z)) is ext-real V14() real Element of REAL
(((((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + ((y * z9) ^2)) + ((y9 * x9) ^2)) - ((2 * (y * z9)) * (y9 * x9)) is ext-real V14() real Element of REAL
x is ext-real V14() real set
z is ext-real V14() real set
x * z is ext-real V14() real set
y is ext-real V14() real set
x9 is ext-real V14() real set
y * x9 is ext-real V14() real set
(x * z) + (y * x9) is ext-real V14() real set
y9 is ext-real V14() real set
z9 is ext-real V14() real set
y9 * z9 is ext-real V14() real set
((x * z) + (y * x9)) + (y9 * z9) is ext-real V14() real set
(((x * z) + (y * x9)) + (y9 * z9)) ^2 is ext-real V14() real set
(((x * z) + (y * x9)) + (y9 * z9)) * (((x * z) + (y * x9)) + (y9 * z9)) is ext-real V14() real set
x ^2 is ext-real V14() real set
x * x is ext-real V14() real set
y ^2 is ext-real V14() real set
y * y is ext-real V14() real set
(x ^2) + (y ^2) is ext-real V14() real set
y9 ^2 is ext-real V14() real set
y9 * y9 is ext-real V14() real set
((x ^2) + (y ^2)) + (y9 ^2) is ext-real V14() real set
z ^2 is ext-real V14() real set
z * z is ext-real V14() real set
x9 ^2 is ext-real V14() real set
x9 * x9 is ext-real V14() real set
(z ^2) + (x9 ^2) is ext-real V14() real set
z9 ^2 is ext-real V14() real set
z9 * z9 is ext-real V14() real set
((z ^2) + (x9 ^2)) + (z9 ^2) is ext-real V14() real set
(((x ^2) + (y ^2)) + (y9 ^2)) * (((z ^2) + (x9 ^2)) + (z9 ^2)) is ext-real V14() real set
x * x9 is ext-real V14() real set
2 * (x * x9) is ext-real V14() real Element of REAL
z * y is ext-real V14() real set
(2 * (x * x9)) * (z * y) is ext-real V14() real Element of REAL
x * z9 is ext-real V14() real set
2 * (x * z9) is ext-real V14() real Element of REAL
y9 * z is ext-real V14() real set
(2 * (x * z9)) * (y9 * z) is ext-real V14() real Element of REAL
((2 * (x * x9)) * (z * y)) + ((2 * (x * z9)) * (y9 * z)) is ext-real V14() real Element of REAL
y * z9 is ext-real V14() real set
2 * (y * z9) is ext-real V14() real Element of REAL
y9 * x9 is ext-real V14() real set
(2 * (y * z9)) * (y9 * x9) is ext-real V14() real Element of REAL
(((2 * (x * x9)) * (z * y)) + ((2 * (x * z9)) * (y9 * z))) + ((2 * (y * z9)) * (y9 * x9)) is ext-real V14() real Element of REAL
(x * x9) ^2 is ext-real V14() real set
(x * x9) * (x * x9) is ext-real V14() real set
(z * y) ^2 is ext-real V14() real set
(z * y) * (z * y) is ext-real V14() real set
((x * x9) ^2) + ((z * y) ^2) is ext-real V14() real set
(x * z9) ^2 is ext-real V14() real set
(x * z9) * (x * z9) is ext-real V14() real set
(((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2) is ext-real V14() real set
(y9 * z) ^2 is ext-real V14() real set
(y9 * z) * (y9 * z) is ext-real V14() real set
((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2) is ext-real V14() real set
(y * z9) ^2 is ext-real V14() real set
(y * z9) * (y * z9) is ext-real V14() real set
(((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + ((y * z9) ^2) is ext-real V14() real set
(y9 * x9) ^2 is ext-real V14() real set
(y9 * x9) * (y9 * x9) is ext-real V14() real set
((((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + ((y * z9) ^2)) + ((y9 * x9) ^2) is ext-real V14() real set
(y9 * z9) ^2 is ext-real V14() real set
(y9 * z9) * (y9 * z9) is ext-real V14() real set
x * y is ext-real V14() real set
2 * (x * y) is ext-real V14() real Element of REAL
z * x9 is ext-real V14() real set
(2 * (x * y)) * (z * x9) is ext-real V14() real Element of REAL
2 * (x * z) is ext-real V14() real Element of REAL
(2 * (x * z)) * (y9 * z9) is ext-real V14() real Element of REAL
((2 * (x * y)) * (z * x9)) + ((2 * (x * z)) * (y9 * z9)) is ext-real V14() real Element of REAL
2 * (y * x9) is ext-real V14() real Element of REAL
(2 * (y * x9)) * (y9 * z9) is ext-real V14() real Element of REAL
(((2 * (x * y)) * (z * x9)) + ((2 * (x * z)) * (y9 * z9))) + ((2 * (y * x9)) * (y9 * z9)) is ext-real V14() real Element of REAL
((y9 * z9) ^2) + ((((2 * (x * y)) * (z * x9)) + ((2 * (x * z)) * (y9 * z9))) + ((2 * (y * x9)) * (y9 * z9))) is ext-real V14() real Element of REAL
(((((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + ((y * z9) ^2)) + ((y9 * x9) ^2)) + ((y9 * z9) ^2) is ext-real V14() real set
(y * x9) ^2 is ext-real V14() real set
(y * x9) * (y * x9) is ext-real V14() real set
((y * x9) ^2) + (((y9 * z9) ^2) + ((((2 * (x * y)) * (z * x9)) + ((2 * (x * z)) * (y9 * z9))) + ((2 * (y * x9)) * (y9 * z9)))) is ext-real V14() real Element of REAL
((((((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + ((y * z9) ^2)) + ((y9 * x9) ^2)) + ((y9 * z9) ^2)) + ((y * x9) ^2) is ext-real V14() real set
(x * z) ^2 is ext-real V14() real set
(x * z) * (x * z) is ext-real V14() real set
((x * z) ^2) + (((y * x9) ^2) + (((y9 * z9) ^2) + ((((2 * (x * y)) * (z * x9)) + ((2 * (x * z)) * (y9 * z9))) + ((2 * (y * x9)) * (y9 * z9))))) is ext-real V14() real Element of REAL
(((((((((x * x9) ^2) + ((z * y) ^2)) + ((x * z9) ^2)) + ((y9 * z) ^2)) + ((y * z9) ^2)) + ((y9 * x9) ^2)) + ((y9 * z9) ^2)) + ((y * x9) ^2)) + ((x * z) ^2) is ext-real V14() real set
x is ext-real V14() real set
y is ext-real V14() real set
z is ext-real V14() real set
x9 is ext-real V14() real set
y9 is ext-real V14() real set
z9 is ext-real V14() real set
x + z is ext-real V14() real set
(x + z) ^2 is ext-real V14() real set
(x + z) * (x + z) is ext-real V14() real set
y + x9 is ext-real V14() real set
(y + x9) ^2 is ext-real V14() real set
(y + x9) * (y + x9) is ext-real V14() real set
((x + z) ^2) + ((y + x9) ^2) is ext-real V14() real set
y9 + z9 is ext-real V14() real set
(y9 + z9) ^2 is ext-real V14() real set
(y9 + z9) * (y9 + z9) is ext-real V14() real set
(((x + z) ^2) + ((y + x9) ^2)) + ((y9 + z9) ^2) is ext-real V14() real set
sqrt ((((x + z) ^2) + ((y + x9) ^2)) + ((y9 + z9) ^2)) is ext-real V14() real set
x ^2 is ext-real V14() real set
x * x is ext-real V14() real set
y ^2 is ext-real V14() real set
y * y is ext-real V14() real set
(x ^2) + (y ^2) is ext-real V14() real set
y9 ^2 is ext-real V14() real set
y9 * y9 is ext-real V14() real set
((x ^2) + (y ^2)) + (y9 ^2) is ext-real V14() real set
sqrt (((x ^2) + (y ^2)) + (y9 ^2)) is ext-real V14() real set
z ^2 is ext-real V14() real set
z * z is ext-real V14() real set
x9 ^2 is ext-real V14() real set
x9 * x9 is ext-real V14() real set
(z ^2) + (x9 ^2) is ext-real V14() real set
z9 ^2 is ext-real V14() real set
z9 * z9 is ext-real V14() real set
((z ^2) + (x9 ^2)) + (z9 ^2) is ext-real V14() real set
sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)) is ext-real V14() real set
(sqrt (((x ^2) + (y ^2)) + (y9 ^2))) + (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))) is ext-real V14() real set
y * x9 is ext-real V14() real set
y9 * z9 is ext-real V14() real set
0 + 0 is ext-real V14() real Element of REAL
(y * x9) + (y9 * z9) is ext-real V14() real set
x * z is ext-real V14() real set
(x * z) + (y * x9) is ext-real V14() real set
((x * z) + (y * x9)) + (y9 * z9) is ext-real V14() real set
(((x * z) + (y * x9)) + (y9 * z9)) ^2 is ext-real V14() real set
(((x * z) + (y * x9)) + (y9 * z9)) * (((x * z) + (y * x9)) + (y9 * z9)) is ext-real V14() real set
sqrt ((((x * z) + (y * x9)) + (y9 * z9)) ^2) is ext-real V14() real set
(((x ^2) + (y ^2)) + (y9 ^2)) * (((z ^2) + (x9 ^2)) + (z9 ^2)) is ext-real V14() real set
sqrt ((((x ^2) + (y ^2)) + (y9 ^2)) * (((z ^2) + (x9 ^2)) + (z9 ^2))) is ext-real V14() real set
(x * z) + ((y * x9) + (y9 * z9)) is ext-real V14() real set
(sqrt (((x ^2) + (y ^2)) + (y9 ^2))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))) is ext-real V14() real set
2 * (((x * z) + (y * x9)) + (y9 * z9)) is ext-real V14() real Element of REAL
2 * ((sqrt (((x ^2) + (y ^2)) + (y9 ^2))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) is ext-real V14() real Element of REAL
2 * ((x * z) + (y * x9)) is ext-real V14() real Element of REAL
2 * (y9 * z9) is ext-real V14() real Element of REAL
(2 * ((x * z) + (y * x9))) + (2 * (y9 * z9)) is ext-real V14() real Element of REAL
((2 * ((x * z) + (y * x9))) + (2 * (y9 * z9))) + (y9 ^2) is ext-real V14() real Element of REAL
2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2))) is ext-real V14() real Element of REAL
(2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))) is ext-real V14() real Element of REAL
((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) + (y9 ^2) is ext-real V14() real Element of REAL
(y9 ^2) + (2 * (y9 * z9)) is ext-real V14() real Element of REAL
(2 * ((x * z) + (y * x9))) + ((y9 ^2) + (2 * (y9 * z9))) is ext-real V14() real Element of REAL
((2 * ((x * z) + (y * x9))) + ((y9 ^2) + (2 * (y9 * z9)))) + (z9 ^2) is ext-real V14() real Element of REAL
(((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) + (y9 ^2)) + (z9 ^2) is ext-real V14() real Element of REAL
2 * (x * z) is ext-real V14() real Element of REAL
2 * (y * x9) is ext-real V14() real Element of REAL
(2 * (x * z)) + (2 * (y * x9)) is ext-real V14() real Element of REAL
((2 * (x * z)) + (2 * (y * x9))) + ((y9 + z9) ^2) is ext-real V14() real Element of REAL
(((2 * (x * z)) + (2 * (y * x9))) + ((y9 + z9) ^2)) + (y ^2) is ext-real V14() real Element of REAL
(y9 ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) is ext-real V14() real Element of REAL
((y9 ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + (z9 ^2) is ext-real V14() real Element of REAL
(((y9 ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + (z9 ^2)) + (y ^2) is ext-real V14() real Element of REAL
(y ^2) + (2 * (y * x9)) is ext-real V14() real Element of REAL
(2 * (x * z)) + ((y ^2) + (2 * (y * x9))) is ext-real V14() real Element of REAL
((2 * (x * z)) + ((y ^2) + (2 * (y * x9)))) + ((y9 + z9) ^2) is ext-real V14() real Element of REAL
(((2 * (x * z)) + ((y ^2) + (2 * (y * x9)))) + ((y9 + z9) ^2)) + (x9 ^2) is ext-real V14() real Element of REAL
(y ^2) + (((y9 ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + (z9 ^2)) is ext-real V14() real Element of REAL
((y ^2) + (((y9 ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + (z9 ^2))) + (x9 ^2) is ext-real V14() real Element of REAL
((y + x9) ^2) + ((y9 + z9) ^2) is ext-real V14() real set
(2 * (x * z)) + (((y + x9) ^2) + ((y9 + z9) ^2)) is ext-real V14() real Element of REAL
(x ^2) + ((2 * (x * z)) + (((y + x9) ^2) + ((y9 + z9) ^2))) is ext-real V14() real Element of REAL
(x9 ^2) + (z9 ^2) is ext-real V14() real set
((y9 ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + ((x9 ^2) + (z9 ^2)) is ext-real V14() real Element of REAL
(y ^2) + (((y9 ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + ((x9 ^2) + (z9 ^2))) is ext-real V14() real Element of REAL
((y ^2) + (((y9 ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + ((x9 ^2) + (z9 ^2)))) + (x ^2) is ext-real V14() real Element of REAL
(x ^2) + (2 * (x * z)) is ext-real V14() real Element of REAL
((x ^2) + (2 * (x * z))) + (((y + x9) ^2) + ((y9 + z9) ^2)) is ext-real V14() real Element of REAL
(((x ^2) + (2 * (x * z))) + (((y + x9) ^2) + ((y9 + z9) ^2))) + (z ^2) is ext-real V14() real Element of REAL
(((x ^2) + (y ^2)) + (y9 ^2)) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) is ext-real V14() real Element of REAL
((((x ^2) + (y ^2)) + (y9 ^2)) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + ((x9 ^2) + (z9 ^2)) is ext-real V14() real Element of REAL
(((((x ^2) + (y ^2)) + (y9 ^2)) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + ((x9 ^2) + (z9 ^2))) + (z ^2) is ext-real V14() real Element of REAL
(z ^2) + ((x9 ^2) + (z9 ^2)) is ext-real V14() real set
((((x ^2) + (y ^2)) + (y9 ^2)) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + ((z ^2) + ((x9 ^2) + (z9 ^2))) is ext-real V14() real Element of REAL
(sqrt (((x ^2) + (y ^2)) + (y9 ^2))) ^2 is ext-real V14() real set
(sqrt (((x ^2) + (y ^2)) + (y9 ^2))) * (sqrt (((x ^2) + (y ^2)) + (y9 ^2))) is ext-real V14() real set
((sqrt (((x ^2) + (y ^2)) + (y9 ^2))) ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) is ext-real V14() real Element of REAL
(((sqrt (((x ^2) + (y ^2)) + (y9 ^2))) ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + (((z ^2) + (x9 ^2)) + (z9 ^2)) is ext-real V14() real Element of REAL
(sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))) ^2 is ext-real V14() real set
(sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))) is ext-real V14() real set
(((sqrt (((x ^2) + (y ^2)) + (y9 ^2))) ^2) + ((2 * (sqrt (((x ^2) + (y ^2)) + (y9 ^2)))) * (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))))) + ((sqrt (((z ^2) + (x9 ^2)) + (z9 ^2))) ^2) is ext-real V14() real Element of REAL
((sqrt (((x ^2) + (y ^2)) + (y9 ^2))) + (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) ^2 is ext-real V14() real set
((sqrt (((x ^2) + (y ^2)) + (y9 ^2))) + (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) * ((sqrt (((x ^2) + (y ^2)) + (y9 ^2))) + (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) is ext-real V14() real set
sqrt (((sqrt (((x ^2) + (y ^2)) + (y9 ^2))) + (sqrt (((z ^2) + (x9 ^2)) + (z9 ^2)))) ^2) is ext-real V14() real set
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
z9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,z9) is ext-real V14() real Element of REAL
y9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,y9) is ext-real V14() real Element of REAL
(x,y,z) . (y9,z9) is ext-real V14() real Element of REAL
((x,y,z) . (x9,y9)) + ((x,y,z) . (y9,z9)) is ext-real V14() real Element of REAL
x9 `1_3 is Element of the carrier of x
y9 `1_3 is Element of the carrier of x
z9 `1_3 is Element of the carrier of x
x9 `2_3 is Element of the carrier of y
y9 `2_3 is Element of the carrier of y
z9 `2_3 is Element of the carrier of y
x9 `3_3 is Element of the carrier of z
y9 `3_3 is Element of the carrier of z
z9 `3_3 is Element of the carrier of z
y1 is Element of the carrier of x
z1 is Element of the carrier of y
d9 is Element of the carrier of z
[y1,z1,d9] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
d6 is Element of the carrier of z
dist (d9,d6) is ext-real V14() real Element of REAL
d5 is Element of the carrier of z
dist (d9,d5) is ext-real V14() real Element of REAL
dist (d5,d6) is ext-real V14() real Element of REAL
y3 is Element of the carrier of x
dist (y1,y3) is ext-real V14() real Element of REAL
y2 is Element of the carrier of x
dist (y1,y2) is ext-real V14() real Element of REAL
dist (y2,y3) is ext-real V14() real Element of REAL
z2 is Element of the carrier of y
[y2,z2,d5] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(dist (d9,d5)) + (dist (d5,d6)) is ext-real V14() real Element of REAL
(dist (d9,d6)) ^2 is ext-real V14() real Element of REAL
(dist (d9,d6)) * (dist (d9,d6)) is ext-real V14() real set
((dist (d9,d5)) + (dist (d5,d6))) ^2 is ext-real V14() real Element of REAL
((dist (d9,d5)) + (dist (d5,d6))) * ((dist (d9,d5)) + (dist (d5,d6))) is ext-real V14() real set
z3 is Element of the carrier of y
dist (z1,z3) is ext-real V14() real Element of REAL
dist (z1,z2) is ext-real V14() real Element of REAL
dist (z2,z3) is ext-real V14() real Element of REAL
[y3,z3,d6] is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(dist (z1,z2)) + (dist (z2,z3)) is ext-real V14() real Element of REAL
(dist (z1,z3)) ^2 is ext-real V14() real Element of REAL
(dist (z1,z3)) * (dist (z1,z3)) is ext-real V14() real set
((dist (z1,z2)) + (dist (z2,z3))) ^2 is ext-real V14() real Element of REAL
((dist (z1,z2)) + (dist (z2,z3))) * ((dist (z1,z2)) + (dist (z2,z3))) is ext-real V14() real set
(dist (y1,y3)) ^2 is ext-real V14() real Element of REAL
(dist (y1,y3)) * (dist (y1,y3)) is ext-real V14() real set
0 + 0 is ext-real V14() real Element of REAL
((dist (y1,y3)) ^2) + ((dist (z1,z3)) ^2) is ext-real V14() real Element of REAL
(dist (y1,y2)) + (dist (y2,y3)) is ext-real V14() real Element of REAL
((dist (y1,y2)) + (dist (y2,y3))) ^2 is ext-real V14() real Element of REAL
((dist (y1,y2)) + (dist (y2,y3))) * ((dist (y1,y2)) + (dist (y2,y3))) is ext-real V14() real set
(((dist (y1,y2)) + (dist (y2,y3))) ^2) + (((dist (z1,z2)) + (dist (z2,z3))) ^2) is ext-real V14() real Element of REAL
(((dist (y1,y3)) ^2) + ((dist (z1,z3)) ^2)) + ((dist (d9,d6)) ^2) is ext-real V14() real Element of REAL
((((dist (y1,y2)) + (dist (y2,y3))) ^2) + (((dist (z1,z2)) + (dist (z2,z3))) ^2)) + (((dist (d9,d5)) + (dist (d5,d6))) ^2) is ext-real V14() real Element of REAL
sqrt ((((dist (y1,y3)) ^2) + ((dist (z1,z3)) ^2)) + ((dist (d9,d6)) ^2)) is ext-real V14() real Element of REAL
sqrt (((((dist (y1,y2)) + (dist (y2,y3))) ^2) + (((dist (z1,z2)) + (dist (z2,z3))) ^2)) + (((dist (d9,d5)) + (dist (d5,d6))) ^2)) is ext-real V14() real Element of REAL
(dist (y1,y2)) ^2 is ext-real V14() real Element of REAL
(dist (y1,y2)) * (dist (y1,y2)) is ext-real V14() real set
(dist (z1,z2)) ^2 is ext-real V14() real Element of REAL
(dist (z1,z2)) * (dist (z1,z2)) is ext-real V14() real set
((dist (y1,y2)) ^2) + ((dist (z1,z2)) ^2) is ext-real V14() real Element of REAL
(dist (d9,d5)) ^2 is ext-real V14() real Element of REAL
(dist (d9,d5)) * (dist (d9,d5)) is ext-real V14() real set
(((dist (y1,y2)) ^2) + ((dist (z1,z2)) ^2)) + ((dist (d9,d5)) ^2) is ext-real V14() real Element of REAL
sqrt ((((dist (y1,y2)) ^2) + ((dist (z1,z2)) ^2)) + ((dist (d9,d5)) ^2)) is ext-real V14() real Element of REAL
(dist (y2,y3)) ^2 is ext-real V14() real Element of REAL
(dist (y2,y3)) * (dist (y2,y3)) is ext-real V14() real set
(dist (z2,z3)) ^2 is ext-real V14() real Element of REAL
(dist (z2,z3)) * (dist (z2,z3)) is ext-real V14() real set
((dist (y2,y3)) ^2) + ((dist (z2,z3)) ^2) is ext-real V14() real Element of REAL
(dist (d5,d6)) ^2 is ext-real V14() real Element of REAL
(dist (d5,d6)) * (dist (d5,d6)) is ext-real V14() real set
(((dist (y2,y3)) ^2) + ((dist (z2,z3)) ^2)) + ((dist (d5,d6)) ^2) is ext-real V14() real Element of REAL
sqrt ((((dist (y2,y3)) ^2) + ((dist (z2,z3)) ^2)) + ((dist (d5,d6)) ^2)) is ext-real V14() real Element of REAL
(sqrt ((((dist (y1,y2)) ^2) + ((dist (z1,z2)) ^2)) + ((dist (d9,d5)) ^2))) + (sqrt ((((dist (y2,y3)) ^2) + ((dist (z2,z3)) ^2)) + ((dist (d5,d6)) ^2))) is ext-real V14() real Element of REAL
((x,y,z) . (x9,y9)) + (sqrt ((((dist (y2,y3)) ^2) + ((dist (z2,z3)) ^2)) + ((dist (d5,d6)) ^2))) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
x9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y9 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (x9,y9) is ext-real V14() real Element of REAL
x is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of x is non empty set
y is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of y is non empty set
z is non empty Reflexive discerning V73() triangle Discerning MetrStruct
the carrier of z is non empty set
[: the carrier of x, the carrier of y, the carrier of z:] is non empty set
(x,y,z) is V23() V26([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:]) V27( REAL ) V28() V37([:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:], REAL ) Element of bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:]
[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:] is non empty V23() set
[:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty V23() set
bool [:[:[: the carrier of x, the carrier of y, the carrier of z:],[: the carrier of x, the carrier of y, the carrier of z:]:],REAL:] is non empty set
MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #) is non empty strict MetrStruct
the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #) is non empty set
x9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #)
y9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #)
z9 is Element of the carrier of MetrStruct(# [: the carrier of x, the carrier of y, the carrier of z:],(x,y,z) #)
dist (x9,y9) is ext-real V14() real Element of REAL
y1 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
y2 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (y1,y2) is ext-real V14() real Element of REAL
dist (y9,x9) is ext-real V14() real Element of REAL
(x,y,z) . (y2,y1) is ext-real V14() real Element of REAL
dist (x9,z9) is ext-real V14() real Element of REAL
y3 is V35() Element of [: the carrier of x, the carrier of y, the carrier of z:]
(x,y,z) . (y1,y3) is ext-real V14() real Element of REAL
dist (y9,z9) is ext-real V14() real Element of REAL
(x,y,z) . (y2,y3) is ext-real V14() real Element of REAL
(dist (x9,y9)) + (dist (y9,z9)) is ext-real V14() real Element of REAL
[:[:REAL,REAL:],[:REAL,REAL:]:] is non empty V23() set
[:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:] is non empty V23() set
bool [:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:] is non empty set
x is V23() V26([:[:REAL,REAL:],[:REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL:],[:REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:]
y is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
[y,x9] is Element of [:REAL,REAL:]
z is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
[z,y9] is Element of [:REAL,REAL:]
real_dist . (y,z) is ext-real V14() real Element of REAL
real_dist . (x9,y9) is ext-real V14() real Element of REAL
(real_dist . (y,z)) + (real_dist . (x9,y9)) is ext-real V14() real Element of REAL
z9 is Element of [:REAL,REAL:]
y1 is Element of [:REAL,REAL:]
x . (z9,y1) is ext-real V14() real Element of REAL
x is V23() V26([:[:REAL,REAL:],[:REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL:],[:REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:]
y is V23() V26([:[:REAL,REAL:],[:REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL:],[:REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:]
z is Element of [:REAL,REAL:]
x9 is Element of [:REAL,REAL:]
x . (z,x9) is ext-real V14() real Element of REAL
y . (z,x9) is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[y9,z9] is Element of [:REAL,REAL:]
y1 is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
[y1,y2] is Element of [:REAL,REAL:]
real_dist . (y9,y1) is ext-real V14() real Element of REAL
real_dist . (z9,y2) is ext-real V14() real Element of REAL
(real_dist . (y9,y1)) + (real_dist . (z9,y2)) is ext-real V14() real Element of REAL
() is V23() V26([:[:REAL,REAL:],[:REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL:],[:REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:]
x is Element of [:REAL,REAL:]
y is Element of [:REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
x `1 is ext-real V14() real Element of REAL
x `2 is ext-real V14() real Element of REAL
y `1 is ext-real V14() real Element of REAL
y `2 is ext-real V14() real Element of REAL
z is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
[z,x9] is Element of [:REAL,REAL:]
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[y9,z9] is Element of [:REAL,REAL:]
real_dist . (x9,z9) is ext-real V14() real Element of REAL
real_dist . (z,y9) is ext-real V14() real Element of REAL
z - y9 is ext-real V14() real Element of REAL
abs (z - y9) is ext-real V14() real Element of REAL
x9 - z9 is ext-real V14() real Element of REAL
abs (x9 - z9) is ext-real V14() real Element of REAL
(real_dist . (z,y9)) + (real_dist . (x9,z9)) is ext-real V14() real Element of REAL
real_dist . (x9,z9) is ext-real V14() real Element of REAL
real_dist . (z,y9) is ext-real V14() real Element of REAL
(real_dist . (z,y9)) + (real_dist . (x9,z9)) is ext-real V14() real Element of REAL
x is Element of [:REAL,REAL:]
y is Element of [:REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
() . (y,x) is ext-real V14() real Element of REAL
x `1 is ext-real V14() real Element of REAL
x `2 is ext-real V14() real Element of REAL
y `1 is ext-real V14() real Element of REAL
y `2 is ext-real V14() real Element of REAL
z is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
[z,x9] is Element of [:REAL,REAL:]
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[y9,z9] is Element of [:REAL,REAL:]
real_dist . (z,y9) is ext-real V14() real Element of REAL
real_dist . (x9,z9) is ext-real V14() real Element of REAL
(real_dist . (z,y9)) + (real_dist . (x9,z9)) is ext-real V14() real Element of REAL
real_dist . (y9,z) is ext-real V14() real Element of REAL
(real_dist . (y9,z)) + (real_dist . (x9,z9)) is ext-real V14() real Element of REAL
real_dist . (z9,x9) is ext-real V14() real Element of REAL
(real_dist . (y9,z)) + (real_dist . (z9,x9)) is ext-real V14() real Element of REAL
x is Element of [:REAL,REAL:]
z is Element of [:REAL,REAL:]
() . (x,z) is ext-real V14() real Element of REAL
y is Element of [:REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
() . (y,z) is ext-real V14() real Element of REAL
(() . (x,y)) + (() . (y,z)) is ext-real V14() real Element of REAL
x `1 is ext-real V14() real Element of REAL
x `2 is ext-real V14() real Element of REAL
y `1 is ext-real V14() real Element of REAL
y `2 is ext-real V14() real Element of REAL
z `1 is ext-real V14() real Element of REAL
z `2 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
[z9,y1] is Element of [:REAL,REAL:]
y9 is ext-real V14() real Element of REAL
real_dist . (y9,y1) is ext-real V14() real Element of REAL
y3 is ext-real V14() real Element of REAL
real_dist . (y1,y3) is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
real_dist . (z9,y2) is ext-real V14() real Element of REAL
real_dist . (y9,y3) is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
real_dist . (x9,y2) is ext-real V14() real Element of REAL
real_dist . (x9,z9) is ext-real V14() real Element of REAL
[y2,y3] is Element of [:REAL,REAL:]
[x9,y9] is Element of [:REAL,REAL:]
(real_dist . (x9,y2)) + (real_dist . (y9,y3)) is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) + (real_dist . (z9,y2)) is ext-real V14() real Element of REAL
(real_dist . (y9,y1)) + (real_dist . (y1,y3)) is ext-real V14() real Element of REAL
((real_dist . (x9,z9)) + (real_dist . (z9,y2))) + ((real_dist . (y9,y1)) + (real_dist . (y1,y3))) is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) + (real_dist . (y9,y1)) is ext-real V14() real Element of REAL
(real_dist . (z9,y2)) + (real_dist . (y1,y3)) is ext-real V14() real Element of REAL
((real_dist . (x9,z9)) + (real_dist . (y9,y1))) + ((real_dist . (z9,y2)) + (real_dist . (y1,y3))) is ext-real V14() real Element of REAL
(() . (x,y)) + ((real_dist . (z9,y2)) + (real_dist . (y1,y3))) is ext-real V14() real Element of REAL
MetrStruct(# [:REAL,REAL:],() #) is non empty strict MetrStruct
the carrier of MetrStruct(# [:REAL,REAL:],() #) is non empty set
x is Element of the carrier of MetrStruct(# [:REAL,REAL:],() #)
y is Element of the carrier of MetrStruct(# [:REAL,REAL:],() #)
z is Element of the carrier of MetrStruct(# [:REAL,REAL:],() #)
dist (x,y) is ext-real V14() real Element of REAL
x9 is Element of [:REAL,REAL:]
y9 is Element of [:REAL,REAL:]
() . (x9,y9) is ext-real V14() real Element of REAL
dist (y,x) is ext-real V14() real Element of REAL
() . (y9,x9) is ext-real V14() real Element of REAL
dist (x,z) is ext-real V14() real Element of REAL
z9 is Element of [:REAL,REAL:]
() . (x9,z9) is ext-real V14() real Element of REAL
dist (y,z) is ext-real V14() real Element of REAL
() . (y9,z9) is ext-real V14() real Element of REAL
(dist (x,y)) + (dist (y,z)) is ext-real V14() real Element of REAL
() is non empty strict Reflexive discerning V73() triangle Discerning MetrStruct
x is V23() V26([:[:REAL,REAL:],[:REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL:],[:REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:]
y is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
[y,x9] is Element of [:REAL,REAL:]
z is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
[z,y9] is Element of [:REAL,REAL:]
real_dist . (y,z) is ext-real V14() real Element of REAL
(real_dist . (y,z)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y,z)) * (real_dist . (y,z)) is ext-real V14() real set
real_dist . (x9,y9) is ext-real V14() real Element of REAL
(real_dist . (x9,y9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,y9)) * (real_dist . (x9,y9)) is ext-real V14() real set
((real_dist . (y,z)) ^2) + ((real_dist . (x9,y9)) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (y,z)) ^2) + ((real_dist . (x9,y9)) ^2)) is ext-real V14() real Element of REAL
z9 is Element of [:REAL,REAL:]
y1 is Element of [:REAL,REAL:]
x . (z9,y1) is ext-real V14() real Element of REAL
x is V23() V26([:[:REAL,REAL:],[:REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL:],[:REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:]
y is V23() V26([:[:REAL,REAL:],[:REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL:],[:REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:]
z is Element of [:REAL,REAL:]
x9 is Element of [:REAL,REAL:]
x . (z,x9) is ext-real V14() real Element of REAL
y . (z,x9) is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[y9,z9] is Element of [:REAL,REAL:]
y1 is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
[y1,y2] is Element of [:REAL,REAL:]
real_dist . (y9,y1) is ext-real V14() real Element of REAL
(real_dist . (y9,y1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,y1)) * (real_dist . (y9,y1)) is ext-real V14() real set
real_dist . (z9,y2) is ext-real V14() real Element of REAL
(real_dist . (z9,y2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z9,y2)) * (real_dist . (z9,y2)) is ext-real V14() real set
((real_dist . (y9,y1)) ^2) + ((real_dist . (z9,y2)) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (y9,y1)) ^2) + ((real_dist . (z9,y2)) ^2)) is ext-real V14() real Element of REAL
() is V23() V26([:[:REAL,REAL:],[:REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL:],[:REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL:],[:REAL,REAL:]:],REAL:]
x is Element of [:REAL,REAL:]
y is Element of [:REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
x `1 is ext-real V14() real Element of REAL
x `2 is ext-real V14() real Element of REAL
y `1 is ext-real V14() real Element of REAL
y `2 is ext-real V14() real Element of REAL
z is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
[z,x9] is Element of [:REAL,REAL:]
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[y9,z9] is Element of [:REAL,REAL:]
real_dist . (x9,z9) is ext-real V14() real Element of REAL
real_dist . (z,y9) is ext-real V14() real Element of REAL
(real_dist . (z,y9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z,y9)) * (real_dist . (z,y9)) is ext-real V14() real set
(real_dist . (x9,z9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) * (real_dist . (x9,z9)) is ext-real V14() real set
((real_dist . (z,y9)) ^2) + ((real_dist . (x9,z9)) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (z,y9)) ^2) + ((real_dist . (x9,z9)) ^2)) is ext-real V14() real Element of REAL
real_dist . (z,y9) is ext-real V14() real Element of REAL
(real_dist . (z,y9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z,y9)) * (real_dist . (z,y9)) is ext-real V14() real set
0 ^2 is ext-real V14() real Element of REAL
0 * 0 is ext-real V14() real set
real_dist . (x9,z9) is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) * (real_dist . (x9,z9)) is ext-real V14() real set
((real_dist . (z,y9)) ^2) + ((real_dist . (x9,z9)) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (z,y9)) ^2) + ((real_dist . (x9,z9)) ^2)) is ext-real V14() real Element of REAL
x is Element of [:REAL,REAL:]
y is Element of [:REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
() . (y,x) is ext-real V14() real Element of REAL
x `1 is ext-real V14() real Element of REAL
x `2 is ext-real V14() real Element of REAL
y `1 is ext-real V14() real Element of REAL
y `2 is ext-real V14() real Element of REAL
z is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
[z,x9] is Element of [:REAL,REAL:]
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[y9,z9] is Element of [:REAL,REAL:]
real_dist . (z,y9) is ext-real V14() real Element of REAL
(real_dist . (z,y9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z,y9)) * (real_dist . (z,y9)) is ext-real V14() real set
real_dist . (x9,z9) is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) * (real_dist . (x9,z9)) is ext-real V14() real set
((real_dist . (z,y9)) ^2) + ((real_dist . (x9,z9)) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (z,y9)) ^2) + ((real_dist . (x9,z9)) ^2)) is ext-real V14() real Element of REAL
real_dist . (y9,z) is ext-real V14() real Element of REAL
(real_dist . (y9,z)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,z)) * (real_dist . (y9,z)) is ext-real V14() real set
((real_dist . (y9,z)) ^2) + ((real_dist . (x9,z9)) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (y9,z)) ^2) + ((real_dist . (x9,z9)) ^2)) is ext-real V14() real Element of REAL
real_dist . (z9,x9) is ext-real V14() real Element of REAL
(real_dist . (z9,x9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z9,x9)) * (real_dist . (z9,x9)) is ext-real V14() real set
((real_dist . (y9,z)) ^2) + ((real_dist . (z9,x9)) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (y9,z)) ^2) + ((real_dist . (z9,x9)) ^2)) is ext-real V14() real Element of REAL
x is Element of [:REAL,REAL:]
z is Element of [:REAL,REAL:]
() . (x,z) is ext-real V14() real Element of REAL
y is Element of [:REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
() . (y,z) is ext-real V14() real Element of REAL
(() . (x,y)) + (() . (y,z)) is ext-real V14() real Element of REAL
x `1 is ext-real V14() real Element of REAL
x `2 is ext-real V14() real Element of REAL
y `1 is ext-real V14() real Element of REAL
y `2 is ext-real V14() real Element of REAL
z `1 is ext-real V14() real Element of REAL
z `2 is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
[x9,y9] is Element of [:REAL,REAL:]
y1 is ext-real V14() real Element of REAL
real_dist . (y9,y1) is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
real_dist . (z9,y2) is ext-real V14() real Element of REAL
real_dist . (x9,y2) is ext-real V14() real Element of REAL
[z9,y1] is Element of [:REAL,REAL:]
y3 is ext-real V14() real Element of REAL
real_dist . (y1,y3) is ext-real V14() real Element of REAL
real_dist . (y9,y3) is ext-real V14() real Element of REAL
real_dist . (x9,z9) is ext-real V14() real Element of REAL
[y2,y3] is Element of [:REAL,REAL:]
y9 - y3 is ext-real V14() real Element of REAL
abs (y9 - y3) is ext-real V14() real Element of REAL
(real_dist . (y9,y3)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,y3)) * (real_dist . (y9,y3)) is ext-real V14() real set
(real_dist . (y9,y1)) + (real_dist . (y1,y3)) is ext-real V14() real Element of REAL
((real_dist . (y9,y1)) + (real_dist . (y1,y3))) ^2 is ext-real V14() real Element of REAL
((real_dist . (y9,y1)) + (real_dist . (y1,y3))) * ((real_dist . (y9,y1)) + (real_dist . (y1,y3))) is ext-real V14() real set
(real_dist . (x9,y2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,y2)) * (real_dist . (x9,y2)) is ext-real V14() real set
0 + 0 is ext-real V14() real Element of REAL
((real_dist . (x9,y2)) ^2) + ((real_dist . (y9,y3)) ^2) is ext-real V14() real Element of REAL
x9 - y2 is ext-real V14() real Element of REAL
abs (x9 - y2) is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) + (real_dist . (z9,y2)) is ext-real V14() real Element of REAL
((real_dist . (x9,z9)) + (real_dist . (z9,y2))) ^2 is ext-real V14() real Element of REAL
((real_dist . (x9,z9)) + (real_dist . (z9,y2))) * ((real_dist . (x9,z9)) + (real_dist . (z9,y2))) is ext-real V14() real set
(((real_dist . (x9,z9)) + (real_dist . (z9,y2))) ^2) + (((real_dist . (y9,y1)) + (real_dist . (y1,y3))) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (x9,y2)) ^2) + ((real_dist . (y9,y3)) ^2)) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (x9,z9)) + (real_dist . (z9,y2))) ^2) + (((real_dist . (y9,y1)) + (real_dist . (y1,y3))) ^2)) is ext-real V14() real Element of REAL
y1 - y3 is ext-real V14() real Element of REAL
abs (y1 - y3) is ext-real V14() real Element of REAL
y9 - y1 is ext-real V14() real Element of REAL
abs (y9 - y1) is ext-real V14() real Element of REAL
z9 - y2 is ext-real V14() real Element of REAL
abs (z9 - y2) is ext-real V14() real Element of REAL
x9 - z9 is ext-real V14() real Element of REAL
abs (x9 - z9) is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,z9)) * (real_dist . (x9,z9)) is ext-real V14() real set
(real_dist . (y9,y1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,y1)) * (real_dist . (y9,y1)) is ext-real V14() real set
((real_dist . (x9,z9)) ^2) + ((real_dist . (y9,y1)) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (x9,z9)) ^2) + ((real_dist . (y9,y1)) ^2)) is ext-real V14() real Element of REAL
(real_dist . (z9,y2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z9,y2)) * (real_dist . (z9,y2)) is ext-real V14() real set
(real_dist . (y1,y3)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y1,y3)) * (real_dist . (y1,y3)) is ext-real V14() real set
((real_dist . (z9,y2)) ^2) + ((real_dist . (y1,y3)) ^2) is ext-real V14() real Element of REAL
sqrt (((real_dist . (z9,y2)) ^2) + ((real_dist . (y1,y3)) ^2)) is ext-real V14() real Element of REAL
(sqrt (((real_dist . (x9,z9)) ^2) + ((real_dist . (y9,y1)) ^2))) + (sqrt (((real_dist . (z9,y2)) ^2) + ((real_dist . (y1,y3)) ^2))) is ext-real V14() real Element of REAL
(() . (x,y)) + (sqrt (((real_dist . (z9,y2)) ^2) + ((real_dist . (y1,y3)) ^2))) is ext-real V14() real Element of REAL
MetrStruct(# [:REAL,REAL:],() #) is non empty strict MetrStruct
the carrier of MetrStruct(# [:REAL,REAL:],() #) is non empty set
x is Element of the carrier of MetrStruct(# [:REAL,REAL:],() #)
y is Element of the carrier of MetrStruct(# [:REAL,REAL:],() #)
z is Element of the carrier of MetrStruct(# [:REAL,REAL:],() #)
dist (x,y) is ext-real V14() real Element of REAL
x9 is Element of [:REAL,REAL:]
y9 is Element of [:REAL,REAL:]
() . (x9,y9) is ext-real V14() real Element of REAL
dist (y,x) is ext-real V14() real Element of REAL
() . (y9,x9) is ext-real V14() real Element of REAL
dist (x,z) is ext-real V14() real Element of REAL
z9 is Element of [:REAL,REAL:]
() . (x9,z9) is ext-real V14() real Element of REAL
dist (y,z) is ext-real V14() real Element of REAL
() . (y9,z9) is ext-real V14() real Element of REAL
(dist (x,y)) + (dist (y,z)) is ext-real V14() real Element of REAL
() is non empty strict Reflexive discerning V73() triangle Discerning MetrStruct
[:REAL,REAL,REAL:] is non empty set
[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:] is non empty V23() set
[:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:] is non empty V23() set
bool [:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:] is non empty set
x is V23() V26([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:]
y is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[y,x9,z9] is V35() Element of [:REAL,REAL,REAL:]
z is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
[z,y9,y1] is V35() Element of [:REAL,REAL,REAL:]
real_dist . (y,z) is ext-real V14() real Element of REAL
real_dist . (x9,y9) is ext-real V14() real Element of REAL
(real_dist . (y,z)) + (real_dist . (x9,y9)) is ext-real V14() real Element of REAL
real_dist . (z9,y1) is ext-real V14() real Element of REAL
((real_dist . (y,z)) + (real_dist . (x9,y9))) + (real_dist . (z9,y1)) is ext-real V14() real Element of REAL
y2 is V35() Element of [:REAL,REAL,REAL:]
y3 is V35() Element of [:REAL,REAL,REAL:]
x . (y2,y3) is ext-real V14() real Element of REAL
x is V23() V26([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:]
y is V23() V26([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:]
z is V35() Element of [:REAL,REAL,REAL:]
x9 is V35() Element of [:REAL,REAL,REAL:]
x . (z,x9) is ext-real V14() real Element of REAL
y . (z,x9) is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
[y9,z9,y1] is V35() Element of [:REAL,REAL,REAL:]
y2 is ext-real V14() real Element of REAL
y3 is ext-real V14() real Element of REAL
z1 is ext-real V14() real Element of REAL
[y2,y3,z1] is V35() Element of [:REAL,REAL,REAL:]
real_dist . (y9,y2) is ext-real V14() real Element of REAL
real_dist . (z9,y3) is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) + (real_dist . (z9,y3)) is ext-real V14() real Element of REAL
real_dist . (y1,z1) is ext-real V14() real Element of REAL
((real_dist . (y9,y2)) + (real_dist . (z9,y3))) + (real_dist . (y1,z1)) is ext-real V14() real Element of REAL
() is V23() V26([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:]
x is V35() Element of [:REAL,REAL,REAL:]
y is V35() Element of [:REAL,REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
x `1_3 is ext-real V14() real Element of REAL
x `2_3 is ext-real V14() real Element of REAL
x `3_3 is ext-real V14() real Element of REAL
y `1_3 is ext-real V14() real Element of REAL
y `2_3 is ext-real V14() real Element of REAL
y `3_3 is ext-real V14() real Element of REAL
z is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
[z,x9,y9] is V35() Element of [:REAL,REAL,REAL:]
z9 is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
[z9,y1,y2] is V35() Element of [:REAL,REAL,REAL:]
real_dist . (y9,y2) is ext-real V14() real Element of REAL
real_dist . (x9,y1) is ext-real V14() real Element of REAL
real_dist . (z,z9) is ext-real V14() real Element of REAL
(real_dist . (z,z9)) + (real_dist . (x9,y1)) is ext-real V14() real Element of REAL
y9 - y2 is ext-real V14() real Element of REAL
abs (y9 - y2) is ext-real V14() real Element of REAL
z - z9 is ext-real V14() real Element of REAL
abs (z - z9) is ext-real V14() real Element of REAL
((real_dist . (z,z9)) + (real_dist . (x9,y1))) + (real_dist . (y9,y2)) is ext-real V14() real Element of REAL
x9 - y1 is ext-real V14() real Element of REAL
abs (x9 - y1) is ext-real V14() real Element of REAL
0 + 0 is ext-real V14() real Element of REAL
real_dist . (z,z9) is ext-real V14() real Element of REAL
real_dist . (x9,y1) is ext-real V14() real Element of REAL
(real_dist . (z,z9)) + (real_dist . (x9,y1)) is ext-real V14() real Element of REAL
real_dist . (y9,y2) is ext-real V14() real Element of REAL
((real_dist . (z,z9)) + (real_dist . (x9,y1))) + (real_dist . (y9,y2)) is ext-real V14() real Element of REAL
x is V35() Element of [:REAL,REAL,REAL:]
y is V35() Element of [:REAL,REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
() . (y,x) is ext-real V14() real Element of REAL
x `1_3 is ext-real V14() real Element of REAL
x `2_3 is ext-real V14() real Element of REAL
x `3_3 is ext-real V14() real Element of REAL
y `1_3 is ext-real V14() real Element of REAL
y `2_3 is ext-real V14() real Element of REAL
y `3_3 is ext-real V14() real Element of REAL
z is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
[z,x9,y9] is V35() Element of [:REAL,REAL,REAL:]
z9 is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
[z9,y1,y2] is V35() Element of [:REAL,REAL,REAL:]
real_dist . (z,z9) is ext-real V14() real Element of REAL
real_dist . (x9,y1) is ext-real V14() real Element of REAL
(real_dist . (z,z9)) + (real_dist . (x9,y1)) is ext-real V14() real Element of REAL
real_dist . (y9,y2) is ext-real V14() real Element of REAL
((real_dist . (z,z9)) + (real_dist . (x9,y1))) + (real_dist . (y9,y2)) is ext-real V14() real Element of REAL
real_dist . (z9,z) is ext-real V14() real Element of REAL
(real_dist . (z9,z)) + (real_dist . (x9,y1)) is ext-real V14() real Element of REAL
((real_dist . (z9,z)) + (real_dist . (x9,y1))) + (real_dist . (y9,y2)) is ext-real V14() real Element of REAL
real_dist . (y1,x9) is ext-real V14() real Element of REAL
(real_dist . (z9,z)) + (real_dist . (y1,x9)) is ext-real V14() real Element of REAL
((real_dist . (z9,z)) + (real_dist . (y1,x9))) + (real_dist . (y9,y2)) is ext-real V14() real Element of REAL
real_dist . (y2,y9) is ext-real V14() real Element of REAL
((real_dist . (z9,z)) + (real_dist . (y1,x9))) + (real_dist . (y2,y9)) is ext-real V14() real Element of REAL
x is V35() Element of [:REAL,REAL,REAL:]
z is V35() Element of [:REAL,REAL,REAL:]
() . (x,z) is ext-real V14() real Element of REAL
y is V35() Element of [:REAL,REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
() . (y,z) is ext-real V14() real Element of REAL
(() . (x,y)) + (() . (y,z)) is ext-real V14() real Element of REAL
x `1_3 is ext-real V14() real Element of REAL
x `2_3 is ext-real V14() real Element of REAL
x `3_3 is ext-real V14() real Element of REAL
y `1_3 is ext-real V14() real Element of REAL
y `2_3 is ext-real V14() real Element of REAL
y `3_3 is ext-real V14() real Element of REAL
z `1_3 is ext-real V14() real Element of REAL
z `2_3 is ext-real V14() real Element of REAL
z `3_3 is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[x9,y9,z9] is V35() Element of [:REAL,REAL,REAL:]
z3 is ext-real V14() real Element of REAL
real_dist . (z9,z3) is ext-real V14() real Element of REAL
y3 is ext-real V14() real Element of REAL
real_dist . (z9,y3) is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
z1 is ext-real V14() real Element of REAL
real_dist . (y1,z1) is ext-real V14() real Element of REAL
z2 is ext-real V14() real Element of REAL
real_dist . (y9,z2) is ext-real V14() real Element of REAL
[z1,z2,z3] is V35() Element of [:REAL,REAL,REAL:]
real_dist . (y3,z3) is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
real_dist . (y9,y2) is ext-real V14() real Element of REAL
real_dist . (y2,z2) is ext-real V14() real Element of REAL
real_dist . (x9,z1) is ext-real V14() real Element of REAL
real_dist . (x9,y1) is ext-real V14() real Element of REAL
[y1,y2,y3] is V35() Element of [:REAL,REAL,REAL:]
(real_dist . (x9,z1)) + (real_dist . (y9,z2)) is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) + (real_dist . (y1,z1)) is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) + (real_dist . (y2,z2)) is ext-real V14() real Element of REAL
((real_dist . (x9,y1)) + (real_dist . (y1,z1))) + ((real_dist . (y9,y2)) + (real_dist . (y2,z2))) is ext-real V14() real Element of REAL
(real_dist . (z9,y3)) + (real_dist . (y3,z3)) is ext-real V14() real Element of REAL
((real_dist . (x9,z1)) + (real_dist . (y9,z2))) + (real_dist . (z9,z3)) is ext-real V14() real Element of REAL
(((real_dist . (x9,y1)) + (real_dist . (y1,z1))) + ((real_dist . (y9,y2)) + (real_dist . (y2,z2)))) + ((real_dist . (z9,y3)) + (real_dist . (y3,z3))) is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) + (real_dist . (y9,y2)) is ext-real V14() real Element of REAL
((real_dist . (x9,y1)) + (real_dist . (y9,y2))) + (real_dist . (z9,y3)) is ext-real V14() real Element of REAL
(real_dist . (y1,z1)) + (real_dist . (y2,z2)) is ext-real V14() real Element of REAL
((real_dist . (y1,z1)) + (real_dist . (y2,z2))) + (real_dist . (y3,z3)) is ext-real V14() real Element of REAL
(((real_dist . (x9,y1)) + (real_dist . (y9,y2))) + (real_dist . (z9,y3))) + (((real_dist . (y1,z1)) + (real_dist . (y2,z2))) + (real_dist . (y3,z3))) is ext-real V14() real Element of REAL
(() . (x,y)) + (((real_dist . (y1,z1)) + (real_dist . (y2,z2))) + (real_dist . (y3,z3))) is ext-real V14() real Element of REAL
MetrStruct(# [:REAL,REAL,REAL:],() #) is non empty strict MetrStruct
the carrier of MetrStruct(# [:REAL,REAL,REAL:],() #) is non empty set
x is Element of the carrier of MetrStruct(# [:REAL,REAL,REAL:],() #)
y is Element of the carrier of MetrStruct(# [:REAL,REAL,REAL:],() #)
z is Element of the carrier of MetrStruct(# [:REAL,REAL,REAL:],() #)
dist (x,y) is ext-real V14() real Element of REAL
x9 is V35() Element of [:REAL,REAL,REAL:]
y9 is V35() Element of [:REAL,REAL,REAL:]
() . (x9,y9) is ext-real V14() real Element of REAL
dist (y,x) is ext-real V14() real Element of REAL
() . (y9,x9) is ext-real V14() real Element of REAL
dist (x,z) is ext-real V14() real Element of REAL
z9 is V35() Element of [:REAL,REAL,REAL:]
() . (x9,z9) is ext-real V14() real Element of REAL
dist (y,z) is ext-real V14() real Element of REAL
() . (y9,z9) is ext-real V14() real Element of REAL
(dist (x,y)) + (dist (y,z)) is ext-real V14() real Element of REAL
() is non empty strict Reflexive discerning V73() triangle Discerning MetrStruct
x is V23() V26([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:]
y is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[y,x9,z9] is V35() Element of [:REAL,REAL,REAL:]
z is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
[z,y9,y1] is V35() Element of [:REAL,REAL,REAL:]
real_dist . (y,z) is ext-real V14() real Element of REAL
(real_dist . (y,z)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y,z)) * (real_dist . (y,z)) is ext-real V14() real set
real_dist . (x9,y9) is ext-real V14() real Element of REAL
(real_dist . (x9,y9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,y9)) * (real_dist . (x9,y9)) is ext-real V14() real set
((real_dist . (y,z)) ^2) + ((real_dist . (x9,y9)) ^2) is ext-real V14() real Element of REAL
real_dist . (z9,y1) is ext-real V14() real Element of REAL
(real_dist . (z9,y1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z9,y1)) * (real_dist . (z9,y1)) is ext-real V14() real set
(((real_dist . (y,z)) ^2) + ((real_dist . (x9,y9)) ^2)) + ((real_dist . (z9,y1)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (y,z)) ^2) + ((real_dist . (x9,y9)) ^2)) + ((real_dist . (z9,y1)) ^2)) is ext-real V14() real Element of REAL
y2 is V35() Element of [:REAL,REAL,REAL:]
y3 is V35() Element of [:REAL,REAL,REAL:]
x . (y2,y3) is ext-real V14() real Element of REAL
x is V23() V26([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:]
y is V23() V26([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:]
z is V35() Element of [:REAL,REAL,REAL:]
x9 is V35() Element of [:REAL,REAL,REAL:]
x . (z,x9) is ext-real V14() real Element of REAL
y . (z,x9) is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
[y9,z9,y1] is V35() Element of [:REAL,REAL,REAL:]
y2 is ext-real V14() real Element of REAL
y3 is ext-real V14() real Element of REAL
z1 is ext-real V14() real Element of REAL
[y2,y3,z1] is V35() Element of [:REAL,REAL,REAL:]
real_dist . (y9,y2) is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) * (real_dist . (y9,y2)) is ext-real V14() real set
real_dist . (z9,y3) is ext-real V14() real Element of REAL
(real_dist . (z9,y3)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z9,y3)) * (real_dist . (z9,y3)) is ext-real V14() real set
((real_dist . (y9,y2)) ^2) + ((real_dist . (z9,y3)) ^2) is ext-real V14() real Element of REAL
real_dist . (y1,z1) is ext-real V14() real Element of REAL
(real_dist . (y1,z1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y1,z1)) * (real_dist . (y1,z1)) is ext-real V14() real set
(((real_dist . (y9,y2)) ^2) + ((real_dist . (z9,y3)) ^2)) + ((real_dist . (y1,z1)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (y9,y2)) ^2) + ((real_dist . (z9,y3)) ^2)) + ((real_dist . (y1,z1)) ^2)) is ext-real V14() real Element of REAL
() is V23() V26([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:]) V27( REAL ) V28() V37([:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:], REAL ) Element of bool [:[:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL:]
x is V35() Element of [:REAL,REAL,REAL:]
y is V35() Element of [:REAL,REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
x `1_3 is ext-real V14() real Element of REAL
x `2_3 is ext-real V14() real Element of REAL
x `3_3 is ext-real V14() real Element of REAL
y `1_3 is ext-real V14() real Element of REAL
y `2_3 is ext-real V14() real Element of REAL
y `3_3 is ext-real V14() real Element of REAL
z is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
[z,x9,y9] is V35() Element of [:REAL,REAL,REAL:]
z9 is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
[z9,y1,y2] is V35() Element of [:REAL,REAL,REAL:]
real_dist . (y9,y2) is ext-real V14() real Element of REAL
real_dist . (x9,y1) is ext-real V14() real Element of REAL
real_dist . (z,z9) is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) * (real_dist . (x9,y1)) is ext-real V14() real set
(real_dist . (y9,y2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) * (real_dist . (y9,y2)) is ext-real V14() real set
(real_dist . (z,z9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z,z9)) * (real_dist . (z,z9)) is ext-real V14() real set
((real_dist . (z,z9)) ^2) + ((real_dist . (x9,y1)) ^2) is ext-real V14() real Element of REAL
(((real_dist . (z,z9)) ^2) + ((real_dist . (x9,y1)) ^2)) + ((real_dist . (y9,y2)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (z,z9)) ^2) + ((real_dist . (x9,y1)) ^2)) + ((real_dist . (y9,y2)) ^2)) is ext-real V14() real Element of REAL
((real_dist . (x9,y1)) ^2) + ((real_dist . (y9,y2)) ^2) is ext-real V14() real Element of REAL
((real_dist . (z,z9)) ^2) + (((real_dist . (x9,y1)) ^2) + ((real_dist . (y9,y2)) ^2)) is ext-real V14() real Element of REAL
sqrt (((real_dist . (z,z9)) ^2) + (((real_dist . (x9,y1)) ^2) + ((real_dist . (y9,y2)) ^2))) is ext-real V14() real Element of REAL
0 + 0 is ext-real V14() real Element of REAL
real_dist . (z,z9) is ext-real V14() real Element of REAL
(real_dist . (z,z9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z,z9)) * (real_dist . (z,z9)) is ext-real V14() real set
0 ^2 is ext-real V14() real Element of REAL
0 * 0 is ext-real V14() real set
real_dist . (x9,y1) is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) * (real_dist . (x9,y1)) is ext-real V14() real set
((real_dist . (z,z9)) ^2) + ((real_dist . (x9,y1)) ^2) is ext-real V14() real Element of REAL
real_dist . (y9,y2) is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) * (real_dist . (y9,y2)) is ext-real V14() real set
(((real_dist . (z,z9)) ^2) + ((real_dist . (x9,y1)) ^2)) + ((real_dist . (y9,y2)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (z,z9)) ^2) + ((real_dist . (x9,y1)) ^2)) + ((real_dist . (y9,y2)) ^2)) is ext-real V14() real Element of REAL
x is V35() Element of [:REAL,REAL,REAL:]
y is V35() Element of [:REAL,REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
() . (y,x) is ext-real V14() real Element of REAL
x `1_3 is ext-real V14() real Element of REAL
x `2_3 is ext-real V14() real Element of REAL
x `3_3 is ext-real V14() real Element of REAL
y `1_3 is ext-real V14() real Element of REAL
y `2_3 is ext-real V14() real Element of REAL
y `3_3 is ext-real V14() real Element of REAL
z is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
[z,x9,y9] is V35() Element of [:REAL,REAL,REAL:]
z9 is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
[z9,y1,y2] is V35() Element of [:REAL,REAL,REAL:]
real_dist . (z,z9) is ext-real V14() real Element of REAL
(real_dist . (z,z9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z,z9)) * (real_dist . (z,z9)) is ext-real V14() real set
real_dist . (x9,y1) is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) * (real_dist . (x9,y1)) is ext-real V14() real set
((real_dist . (z,z9)) ^2) + ((real_dist . (x9,y1)) ^2) is ext-real V14() real Element of REAL
real_dist . (y9,y2) is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) * (real_dist . (y9,y2)) is ext-real V14() real set
(((real_dist . (z,z9)) ^2) + ((real_dist . (x9,y1)) ^2)) + ((real_dist . (y9,y2)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (z,z9)) ^2) + ((real_dist . (x9,y1)) ^2)) + ((real_dist . (y9,y2)) ^2)) is ext-real V14() real Element of REAL
real_dist . (z9,z) is ext-real V14() real Element of REAL
(real_dist . (z9,z)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z9,z)) * (real_dist . (z9,z)) is ext-real V14() real set
((real_dist . (z9,z)) ^2) + ((real_dist . (x9,y1)) ^2) is ext-real V14() real Element of REAL
(((real_dist . (z9,z)) ^2) + ((real_dist . (x9,y1)) ^2)) + ((real_dist . (y9,y2)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (z9,z)) ^2) + ((real_dist . (x9,y1)) ^2)) + ((real_dist . (y9,y2)) ^2)) is ext-real V14() real Element of REAL
real_dist . (y1,x9) is ext-real V14() real Element of REAL
(real_dist . (y1,x9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y1,x9)) * (real_dist . (y1,x9)) is ext-real V14() real set
((real_dist . (z9,z)) ^2) + ((real_dist . (y1,x9)) ^2) is ext-real V14() real Element of REAL
(((real_dist . (z9,z)) ^2) + ((real_dist . (y1,x9)) ^2)) + ((real_dist . (y9,y2)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (z9,z)) ^2) + ((real_dist . (y1,x9)) ^2)) + ((real_dist . (y9,y2)) ^2)) is ext-real V14() real Element of REAL
real_dist . (y2,y9) is ext-real V14() real Element of REAL
(real_dist . (y2,y9)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y2,y9)) * (real_dist . (y2,y9)) is ext-real V14() real set
(((real_dist . (z9,z)) ^2) + ((real_dist . (y1,x9)) ^2)) + ((real_dist . (y2,y9)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (z9,z)) ^2) + ((real_dist . (y1,x9)) ^2)) + ((real_dist . (y2,y9)) ^2)) is ext-real V14() real Element of REAL
x is V35() Element of [:REAL,REAL,REAL:]
z is V35() Element of [:REAL,REAL,REAL:]
() . (x,z) is ext-real V14() real Element of REAL
y is V35() Element of [:REAL,REAL,REAL:]
() . (x,y) is ext-real V14() real Element of REAL
() . (y,z) is ext-real V14() real Element of REAL
(() . (x,y)) + (() . (y,z)) is ext-real V14() real Element of REAL
x `1_3 is ext-real V14() real Element of REAL
x `2_3 is ext-real V14() real Element of REAL
x `3_3 is ext-real V14() real Element of REAL
y `1_3 is ext-real V14() real Element of REAL
y `2_3 is ext-real V14() real Element of REAL
y `3_3 is ext-real V14() real Element of REAL
z `1_3 is ext-real V14() real Element of REAL
z `2_3 is ext-real V14() real Element of REAL
z `3_3 is ext-real V14() real Element of REAL
x9 is ext-real V14() real Element of REAL
y9 is ext-real V14() real Element of REAL
z9 is ext-real V14() real Element of REAL
[x9,y9,z9] is V35() Element of [:REAL,REAL,REAL:]
y3 is ext-real V14() real Element of REAL
z3 is ext-real V14() real Element of REAL
real_dist . (y3,z3) is ext-real V14() real Element of REAL
y2 is ext-real V14() real Element of REAL
real_dist . (y9,y2) is ext-real V14() real Element of REAL
z2 is ext-real V14() real Element of REAL
real_dist . (y2,z2) is ext-real V14() real Element of REAL
z1 is ext-real V14() real Element of REAL
real_dist . (x9,z1) is ext-real V14() real Element of REAL
y1 is ext-real V14() real Element of REAL
real_dist . (x9,y1) is ext-real V14() real Element of REAL
[y1,y2,y3] is V35() Element of [:REAL,REAL,REAL:]
y3 - z3 is ext-real V14() real Element of REAL
abs (y3 - z3) is ext-real V14() real Element of REAL
y2 - z2 is ext-real V14() real Element of REAL
abs (y2 - z2) is ext-real V14() real Element of REAL
y9 - y2 is ext-real V14() real Element of REAL
abs (y9 - y2) is ext-real V14() real Element of REAL
real_dist . (z9,z3) is ext-real V14() real Element of REAL
real_dist . (z9,y3) is ext-real V14() real Element of REAL
real_dist . (y1,z1) is ext-real V14() real Element of REAL
real_dist . (y9,z2) is ext-real V14() real Element of REAL
[z1,z2,z3] is V35() Element of [:REAL,REAL,REAL:]
z9 - z3 is ext-real V14() real Element of REAL
abs (z9 - z3) is ext-real V14() real Element of REAL
(real_dist . (z9,z3)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z9,z3)) * (real_dist . (z9,z3)) is ext-real V14() real set
(real_dist . (z9,y3)) + (real_dist . (y3,z3)) is ext-real V14() real Element of REAL
((real_dist . (z9,y3)) + (real_dist . (y3,z3))) ^2 is ext-real V14() real Element of REAL
((real_dist . (z9,y3)) + (real_dist . (y3,z3))) * ((real_dist . (z9,y3)) + (real_dist . (y3,z3))) is ext-real V14() real set
y9 - z2 is ext-real V14() real Element of REAL
abs (y9 - z2) is ext-real V14() real Element of REAL
(real_dist . (y9,z2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,z2)) * (real_dist . (y9,z2)) is ext-real V14() real set
(real_dist . (y9,y2)) + (real_dist . (y2,z2)) is ext-real V14() real Element of REAL
((real_dist . (y9,y2)) + (real_dist . (y2,z2))) ^2 is ext-real V14() real Element of REAL
((real_dist . (y9,y2)) + (real_dist . (y2,z2))) * ((real_dist . (y9,y2)) + (real_dist . (y2,z2))) is ext-real V14() real set
x9 - z1 is ext-real V14() real Element of REAL
abs (x9 - z1) is ext-real V14() real Element of REAL
(real_dist . (x9,z1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,z1)) * (real_dist . (x9,z1)) is ext-real V14() real set
(real_dist . (x9,y1)) + (real_dist . (y1,z1)) is ext-real V14() real Element of REAL
((real_dist . (x9,y1)) + (real_dist . (y1,z1))) ^2 is ext-real V14() real Element of REAL
((real_dist . (x9,y1)) + (real_dist . (y1,z1))) * ((real_dist . (x9,y1)) + (real_dist . (y1,z1))) is ext-real V14() real set
((real_dist . (x9,z1)) ^2) + ((real_dist . (y9,z2)) ^2) is ext-real V14() real Element of REAL
(((real_dist . (x9,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (y9,y2)) + (real_dist . (y2,z2))) ^2) is ext-real V14() real Element of REAL
(((real_dist . (x9,z1)) ^2) + ((real_dist . (y9,z2)) ^2)) + ((real_dist . (z9,z3)) ^2) is ext-real V14() real Element of REAL
((((real_dist . (x9,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (y9,y2)) + (real_dist . (y2,z2))) ^2)) + (((real_dist . (z9,y3)) + (real_dist . (y3,z3))) ^2) is ext-real V14() real Element of REAL
0 + 0 is ext-real V14() real Element of REAL
sqrt ((((real_dist . (x9,z1)) ^2) + ((real_dist . (y9,z2)) ^2)) + ((real_dist . (z9,z3)) ^2)) is ext-real V14() real Element of REAL
sqrt (((((real_dist . (x9,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (y9,y2)) + (real_dist . (y2,z2))) ^2)) + (((real_dist . (z9,y3)) + (real_dist . (y3,z3))) ^2)) is ext-real V14() real Element of REAL
z9 - y3 is ext-real V14() real Element of REAL
abs (z9 - y3) is ext-real V14() real Element of REAL
y1 - z1 is ext-real V14() real Element of REAL
abs (y1 - z1) is ext-real V14() real Element of REAL
x9 - y1 is ext-real V14() real Element of REAL
abs (x9 - y1) is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (x9,y1)) * (real_dist . (x9,y1)) is ext-real V14() real set
(real_dist . (y9,y2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y9,y2)) * (real_dist . (y9,y2)) is ext-real V14() real set
((real_dist . (x9,y1)) ^2) + ((real_dist . (y9,y2)) ^2) is ext-real V14() real Element of REAL
(real_dist . (z9,y3)) ^2 is ext-real V14() real Element of REAL
(real_dist . (z9,y3)) * (real_dist . (z9,y3)) is ext-real V14() real set
(((real_dist . (x9,y1)) ^2) + ((real_dist . (y9,y2)) ^2)) + ((real_dist . (z9,y3)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (x9,y1)) ^2) + ((real_dist . (y9,y2)) ^2)) + ((real_dist . (z9,y3)) ^2)) is ext-real V14() real Element of REAL
(real_dist . (y1,z1)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y1,z1)) * (real_dist . (y1,z1)) is ext-real V14() real set
(real_dist . (y2,z2)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y2,z2)) * (real_dist . (y2,z2)) is ext-real V14() real set
((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2) is ext-real V14() real Element of REAL
(real_dist . (y3,z3)) ^2 is ext-real V14() real Element of REAL
(real_dist . (y3,z3)) * (real_dist . (y3,z3)) is ext-real V14() real set
(((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2)) + ((real_dist . (y3,z3)) ^2) is ext-real V14() real Element of REAL
sqrt ((((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2)) + ((real_dist . (y3,z3)) ^2)) is ext-real V14() real Element of REAL
(sqrt ((((real_dist . (x9,y1)) ^2) + ((real_dist . (y9,y2)) ^2)) + ((real_dist . (z9,y3)) ^2))) + (sqrt ((((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2)) + ((real_dist . (y3,z3)) ^2))) is ext-real V14() real Element of REAL
(() . (x,y)) + (sqrt ((((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2)) + ((real_dist . (y3,z3)) ^2))) is ext-real V14() real Element of REAL
MetrStruct(# [:REAL,REAL,REAL:],() #) is non empty strict MetrStruct
the carrier of MetrStruct(# [:REAL,REAL,REAL:],() #) is non empty set
x is Element of the carrier of MetrStruct(# [:REAL,REAL,REAL:],() #)
y is Element of the carrier of MetrStruct(# [:REAL,REAL,REAL:],() #)
z is Element of the carrier of MetrStruct(# [:REAL,REAL,REAL:],() #)
dist (x,y) is ext-real V14() real Element of REAL
x9 is V35() Element of [:REAL,REAL,REAL:]
y9 is V35() Element of [:REAL,REAL,REAL:]
() . (x9,y9) is ext-real V14() real Element of REAL
dist (y,x) is ext-real V14() real Element of REAL
() . (y9,x9) is ext-real V14() real Element of REAL
dist (x,z) is ext-real V14() real Element of REAL
z9 is V35() Element of [:REAL,REAL,REAL:]
() . (x9,z9) is ext-real V14() real Element of REAL
dist (y,z) is ext-real V14() real Element of REAL
() . (y9,z9) is ext-real V14() real Element of REAL
(dist (x,y)) + (dist (y,z)) is ext-real V14() real Element of REAL
() is non empty strict Reflexive discerning V73() triangle Discerning MetrStruct