:: 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
is non empty V23() set
is non empty V23() set
bool 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

F3() is non empty set
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is non empty V23() set
[:[:F1(),F2():],[:F1(),F2():]:] is non empty V23() set
[:[:[:F1(),F2():],[:F1(),F2():]:],F3():] is non empty V23() set
bool [:[:[:F1(),F2():],[:F1(),F2():]:],F3():] is non empty set
x is V23() V26([:[:F1(),F2():],[:F1(),F2():]:]) V27(F3()) V28() V37([:[:F1(),F2():],[:F1(),F2():]:],F3()) Element of bool [:[:[:F1(),F2():],[:F1(),F2():]:],F3():]
y is Element of F1()
z is Element of F1()
x9 is Element of F2()
[y,x9] is Element of [:F1(),F2():]
y9 is Element of F2()
[z,y9] is Element of [:F1(),F2():]
F4(y,z,x9,y9) is Element of F3()
z9 is Element of [:F1(),F2():]
y1 is Element of [:F1(),F2():]
x . (z9,y1) is Element of F3()
y1 `1 is Element of F1()
y1 `2 is Element of F2()
[(y1 `1),(y1 `2)] is Element of [:F1(),F2():]
z9 `1 is Element of F1()
z9 `2 is Element of F2()
[(z9 `1),(z9 `2)] is Element of [:F1(),F2():]

the carrier of x is non empty set

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

the carrier of x is non empty set

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

the carrier of x is non empty set

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

the carrier of x is non empty set

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

the carrier of x is non empty set

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

the carrier of x is non empty set

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
F4() is non empty set
F1() is non empty set
F2() is non empty set
F3() is non empty set
[:F1(),F2(),F3():] is non empty set
[:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:] is non empty V23() set
[:[:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:],F4():] is non empty V23() set
bool [:[:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:],F4():] is non empty set
x is V23() V26([:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:]) V27(F4()) V28() V37([:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:],F4()) Element of bool [:[:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:],F4():]
y is Element of F1()
z is Element of F1()
x9 is Element of F2()
y9 is Element of F2()
z9 is Element of F3()
[y,x9,z9] is V35() Element of [:F1(),F2(),F3():]
y1 is Element of F3()
[z,y9,y1] is V35() Element of [:F1(),F2(),F3():]
F5(y,z,x9,y9,z9,y1) is Element of F4()
y2 is V35() Element of [:F1(),F2(),F3():]
y3 is V35() Element of [:F1(),F2(),F3():]
x . (y2,y3) is Element of F4()
y3 `1_3 is Element of F1()
y3 `2_3 is Element of F2()
y3 `3_3 is Element of F3()
[(y3 `1_3),(y3 `2_3),(y3 `3_3)] is V35() Element of [:F1(),F2(),F3():]
y2 `1_3 is Element of F1()
y2 `2_3 is Element of F2()
y2 `3_3 is Element of F3()
[(y2 `1_3),(y2 `2_3),(y2 `3_3)] is V35() Element of [:F1(),F2(),F3():]

the carrier of x is non empty set

the carrier of y is non empty set

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

the carrier of x is non empty set

the carrier of y is non empty set

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

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

the carrier of x is non empty set

the carrier of y is non empty set

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

the carrier of x is non empty set

the carrier of y is non empty set

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

the carrier of x is non empty set

the carrier of y is non empty set

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

the carrier of x is non empty set

the carrier of y is non empty set

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
F5() is non empty set
F1() is non empty set
F2() is non empty set
F3() is non empty set
F4() is non empty set
[:F1(),F2(),F3(),F4():] is non empty set
[:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:] is non empty V23() set
[:[:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:],F5():] is non empty V23() set
bool [:[:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:],F5():] is non empty set
x is V23() V26([:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:]) V27(F5()) V28() V37([:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:],F5()) Element of bool [:[:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:],F5():]
y is Element of F1()
z is Element of F1()
x9 is Element of F2()
y9 is Element of F2()
z9 is Element of F3()
y1 is Element of F3()
y2 is Element of F4()
[y,x9,z9,y2] is V36() Element of [:F1(),F2(),F3(),F4():]
y3 is Element of F4()
[z,y9,y1,y3] is V36() Element of [:F1(),F2(),F3(),F4():]
F6(y,z,x9,y9,z9,y1,y2,y3) is Element of F5()
z1 is V36() Element of [:F1(),F2(),F3(),F4():]
z2 is V36() Element of [:F1(),F2(),F3(),F4():]
x . (z1,z2) is Element of F5()
z2 `1_4 is Element of F1()
z2 `2_4 is Element of F2()
z2 `3_4 is Element of F3()
z2 `4_4 is Element of F4()
[(z2 `1_4),(z2 `2_4),(z2 `3_4),(z2 `4_4)] is V36() Element of [:F1(),F2(),F3(),F4():]
z1 `1_4 is Element of F1()
z1 `2_4 is Element of F2()
z1 `3_4 is Element of F3()
z1 `4_4 is Element of F4()
[(z1 `1_4),(z1 `2_4),(z1 `3_4),(z1 `4_4)] is V36() Element of [:F1(),F2(),F3(),F4():]

the carrier of x is non empty set

the carrier of y is non empty set

the carrier of z is non empty set

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

the carrier of x is non empty set

the carrier of y is non empty set

the carrier of z is non empty set

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

((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

the carrier of x is non empty set

the carrier of y is non empty set

the carrier of z is non empty set

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

the carrier of x is non empty set

the carrier of y is non empty set

the carrier of z is non empty set

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

the carrier of x is non empty set

the carrier of y is non empty set

the carrier of z is non empty set

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

the carrier of x is non empty set

the carrier of y is non empty set

the carrier of z is non empty set

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

the carrier of x is non empty set

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

the carrier of x is non empty set

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

dist (y1,y2) is ext-real V14() real Element of REAL
(