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

F

F

[:F

[:[:F

[:[:[:F

bool [:[:[:F

x is V23() V26([:[:F

y is Element of F

z is Element of F

x9 is Element of F

[y,x9] is Element of [:F

y9 is Element of F

[z,y9] is Element of [:F

F

z9 is Element of [:F

y1 is Element of [:F

x . (z9,y1) is Element of F

y1 `1 is Element of F

y1 `2 is Element of F

[(y1 `1),(y1 `2)] is Element of [:F

z9 `1 is Element of F

z9 `2 is Element of F

[(z9 `1),(z9 `2)] is Element of [: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

F

F

F

[:F

[:[:F

[:[:[:F

bool [:[:[:F

x is V23() V26([:[: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

y1 is Element of F

[z,y9,y1] is V35() Element of [:F

F

y2 is V35() Element of [:F

y3 is V35() Element of [:F

x . (y2,y3) is Element of F

y3 `1_3 is Element of F

y3 `2_3 is Element of F

y3 `3_3 is Element of F

[(y3 `1_3),(y3 `2_3),(y3 `3_3)] is V35() Element of [:F

y2 `1_3 is Element of F

y2 `2_3 is Element of F

y2 `3_3 is Element of F

[(y2 `1_3),(y2 `2_3),(y2 `3_3)] is V35() Element of [: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

F

F

F

F

[:F

[:[:F

[:[:[:F

bool [:[:[:F

x is V23() V26([:[: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

y1 is Element of F

y2 is Element of F

[y,x9,z9,y2] is V36() Element of [:F

y3 is Element of F

[z,y9,y1,y3] is V36() Element of [:F

F

z1 is V36() Element of [:F

z2 is V36() Element of [:F

x . (z1,z2) is Element of F

z2 `1_4 is Element of F

z2 `2_4 is Element of F

z2 `3_4 is Element of F

z2 `4_4 is Element of F

[(z2 `1_4),(z2 `2_4),(z2 `3_4),(z2 `4_4)] is V36() Element of [:F

z1 `1_4 is Element of F

z1 `2_4 is Element of F

z1 `3_4 is Element of F

z1 `4_4 is Element of F

[(z1 `1_4),(z1 `2_4),(z1 `3_4),(z1 `4_4)] is V36() Element of [: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

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

(