:: METRIC_2 semantic presentation

REAL is non empty V29() V30() V31() V35() V43() set

bool REAL is non empty set

NAT is V29() V30() V31() V32() V33() V34() V35() Element of bool REAL

NAT is V29() V30() V31() V32() V33() V34() V35() set

bool NAT is non empty set

1 is non empty set

[:1,1:] is non empty set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is non empty set

bool [:[:1,1:],1:] is non empty set

[:[:1,1:],REAL:] is non empty set

bool [:[:1,1:],REAL:] is non empty set

[:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty set

bool [:[:REAL,REAL:],REAL:] is non empty set

2 is non empty set

[:2,2:] is non empty set

[:[:2,2:],REAL:] is non empty set

bool [:[:2,2:],REAL:] is non empty set

{} is empty V29() V30() V31() V32() V33() V34() V35() set

0 is empty ext-real non positive non negative V26() V27() V28() V29() V30() V31() V32() V33() V34() V35() Element of NAT

M is non empty MetrStruct

the carrier of M is non empty set

M is non empty Reflexive MetrStruct

the carrier of M is non empty set

Q is Element of the carrier of M

dist (Q,Q) is ext-real V27() V28() Element of REAL

M is non empty symmetric MetrStruct

the carrier of M is non empty set

Q is Element of the carrier of M

W is Element of the carrier of M

dist (Q,W) is ext-real V27() V28() Element of REAL

M is non empty MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

{ b

bool the carrier of M is non empty set

{ b

M is non empty MetrStruct

the carrier of M is non empty set

bool the carrier of M is non empty set

the Element of the carrier of M is Element of the carrier of M

(M, the Element of the carrier of M) is Element of bool the carrier of M

{ b

M is non empty Reflexive MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

V is Element of the carrier of M

Q is Element of the carrier of M

dist (Z,V) is ext-real V27() V28() Element of REAL

dist (V,Q) is ext-real V27() V28() Element of REAL

dist (Z,Q) is ext-real V27() V28() Element of REAL

0 + 0 is empty ext-real non positive non negative V27() V28() V29() V30() V31() V32() V33() V34() V35() set

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

V is Element of the carrier of M

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

Q is Element of the carrier of M

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

V is Element of the carrier of M

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

Q is Element of the carrier of M

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

V is Element of the carrier of M

(M,V) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

(M,Z) is Element of bool the carrier of M

{ b

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

V is Element of the carrier of M

(M,V) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

Q is Element of the carrier of M

(M,Q) is Element of bool the carrier of M

{ b

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

V is Element of the carrier of M

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

(M,V) is Element of bool the carrier of M

{ b

Q is Element of the carrier of M

Q is Element of the carrier of M

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

V is Element of the carrier of M

(M,V) is Element of bool the carrier of M

{ b

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

V is Element of the carrier of M

(M,V) is Element of bool the carrier of M

{ b

Q is set

W is Element of the carrier of M

V9 is Element of the carrier of M

Q9 is Element of the carrier of M

M is non empty Reflexive symmetric triangle MetrStruct

Z is (M)

the carrier of M is non empty set

V is Element of the carrier of M

(M,V) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

M is non empty Reflexive symmetric triangle MetrStruct

Z is (M)

M is non empty Reflexive symmetric triangle MetrStruct

the carrier of M is non empty set

V is Element of the carrier of M

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

Q is Element of the carrier of M

dist (V,Q) is ext-real V27() V28() Element of REAL

M is non empty Reflexive discerning MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

V is Element of the carrier of M

dist (Z,V) is ext-real V27() V28() Element of REAL

M is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of M is non empty set

V is Element of the carrier of M

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

Q is Element of the carrier of M

M is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

{Z} is non empty Element of bool the carrier of M

V is Element of the carrier of M

V is Element of the carrier of M

M is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of M is non empty set

bool the carrier of M is non empty set

Z is Element of bool the carrier of M

V is Element of the carrier of M

(M,V) is Element of bool the carrier of M

{ b

{V} is non empty Element of bool the carrier of M

V is Element of the carrier of M

{V} is non empty Element of bool the carrier of M

(M,V) is Element of bool the carrier of M

{ b

V is Element of the carrier of M

{V} is non empty Element of bool the carrier of M

Q is Element of the carrier of M

{Q} is non empty Element of bool the carrier of M

M is non empty MetrStruct

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

M is non empty MetrStruct

(M) is set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

the Element of the carrier of M is Element of the carrier of M

(M, the Element of the carrier of M) is Element of bool the carrier of M

{ b

M is set

Z is non empty MetrStruct

(Z) is non empty set

the carrier of Z is non empty set

bool the carrier of Z is non empty set

{ b

V is Element of bool the carrier of Z

Q is Element of the carrier of Z

(Z,Q) is Element of bool the carrier of Z

{ b

V is Element of the carrier of Z

(Z,V) is Element of bool the carrier of Z

{ b

Q is Element of the carrier of Z

(Z,Q) is Element of bool the carrier of Z

{ b

M is non empty MetrStruct

the carrier of M is non empty set

Z is Element of the carrier of M

(M,Z) is Element of bool the carrier of M

bool the carrier of M is non empty set

{ b

(M) is non empty set

{ b

M is set

Z is non empty MetrStruct

(Z) is non empty set

the carrier of Z is non empty set

bool the carrier of Z is non empty set

{ b

V is Element of the carrier of Z

(Z,V) is Element of bool the carrier of Z

{ b

V is Element of the carrier of Z

(Z,V) is Element of bool the carrier of Z

{ b

M is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of M is non empty set

(M) is non empty set

bool the carrier of M is non empty set

{ b

Z is Element of the carrier of M

{Z} is non empty Element of bool the carrier of M

(M,Z) is Element of bool the carrier of M

{ b

M is set

Z is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

(Z) is non empty set

the carrier of Z is non empty set

bool the carrier of Z is non empty set

{ b

V is Element of the carrier of Z

(Z,V) is Element of bool the carrier of Z

{ b

{V} is non empty Element of bool the carrier of Z

V is Element of the carrier of Z

{V} is non empty Element of bool the carrier of Z

(Z,V) is Element of bool the carrier of Z

{ b

V is Element of the carrier of Z

{V} is non empty Element of bool the carrier of Z

Q is Element of the carrier of Z

{Q} is non empty Element of bool the carrier of Z

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

Z is Element of (M)

V is Element of (M)

Q is Element of the carrier of M

V9 is Element of the carrier of M

W is Element of the carrier of M

Q9 is Element of the carrier of M

dist (Q,V9) is ext-real V27() V28() Element of REAL

dist (W,Q9) is ext-real V27() V28() Element of REAL

dist (Q,W) is ext-real V27() V28() Element of REAL

W9 is Element of the carrier of M

(M,W9) is Element of bool the carrier of M

{ b

dist (V9,Q9) is ext-real V27() V28() Element of REAL

W9 is Element of the carrier of M

(M,W9) is Element of bool the carrier of M

{ b

dist (W,Q) is ext-real V27() V28() Element of REAL

dist (Q,Q9) is ext-real V27() V28() Element of REAL

(dist (W,Q)) + (dist (Q,Q9)) is ext-real V27() V28() set

(dist (Q,V9)) + (dist (V9,Q9)) is ext-real V27() V28() set

dist (W,V9) is ext-real V27() V28() Element of REAL

(dist (Q,W)) + (dist (W,V9)) is ext-real V27() V28() set

dist (Q9,V9) is ext-real V27() V28() Element of REAL

(dist (W,Q9)) + (dist (Q9,V9)) is ext-real V27() V28() set

M is non empty MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

Z is Element of (M)

V is Element of (M)

Q is ext-real V27() V28() Element of REAL

W is Element of the carrier of M

(M,W) is Element of bool the carrier of M

{ b

V9 is Element of the carrier of M

(M,V9) is Element of bool the carrier of M

{ b

dist (V9,W) is ext-real V27() V28() Element of REAL

W is Element of the carrier of M

V9 is Element of the carrier of M

dist (W,V9) is ext-real V27() V28() Element of REAL

Q9 is Element of the carrier of M

W9 is Element of the carrier of M

dist (Q9,W9) is ext-real V27() V28() Element of REAL

W is Element of the carrier of M

V9 is Element of the carrier of M

dist (W,V9) is ext-real V27() V28() Element of REAL

Q9 is Element of the carrier of M

W9 is Element of the carrier of M

dist (Q9,W9) is ext-real V27() V28() Element of REAL

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

Z is Element of (M)

V is Element of (M)

Q is ext-real V27() V28() Element of REAL

W is Element of the carrier of M

V9 is Element of the carrier of M

dist (W,V9) is ext-real V27() V28() Element of REAL

M is non empty MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

Z is Element of (M)

V is Element of (M)

{ b

{ b

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

Z is Element of (M)

V is Element of (M)

(M,Z,V) is V29() V30() V31() Element of bool REAL

{ b

Q is ext-real V27() V28() Element of REAL

W is ext-real V27() V28() Element of REAL

M is non empty MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

[:(M),(M):] is non empty set

Z is ext-real V27() V28() Element of REAL

{ b

( b

bool [:(M),(M):] is non empty set

{ b

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

[:(M),(M):] is non empty set

Z is ext-real V27() V28() Element of REAL

(M,Z) is Element of bool [:(M),(M):]

bool [:(M),(M):] is non empty set

{ b

( b

V is Element of [:(M),(M):]

Q is Element of [:(M),(M):]

W is Element of (M)

V9 is Element of (M)

[W,V9] is Element of [:(M),(M):]

Q is Element of (M)

W is Element of (M)

[Q,W] is Element of [:(M),(M):]

V9 is Element of (M)

Q9 is Element of (M)

[V9,Q9] is Element of [:(M),(M):]

M is non empty MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

{ b

{ b

M is non empty Reflexive symmetric triangle MetrStruct

(M) is V29() V30() V31() Element of bool REAL

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

{ b

Z is ext-real V27() V28() Element of REAL

V is ext-real V27() V28() Element of REAL

Q is Element of (M)

W is Element of (M)

V is Element of (M)

Q is Element of (M)

W is Element of (M)

V9 is Element of (M)

M is non empty MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

{ b

for b

bool (M) is non empty set

{ b

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

(M) is Element of bool (M)

bool (M) is non empty set

{ b

for b

Z is Element of (M)

V is Element of (M)

Q is Element of (M)

W is ext-real V27() V28() Element of REAL

V is Element of (M)

Q is ext-real V27() V28() Element of REAL

W is Element of (M)

V9 is ext-real V27() V28() Element of REAL

M is non empty MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

{ b

for b

bool (M) is non empty set

{ b

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

(M) is Element of bool (M)

bool (M) is non empty set

{ b

for b

Z is Element of (M)

V is Element of (M)

Q is Element of (M)

W is ext-real V27() V28() Element of REAL

V is Element of (M)

Q is ext-real V27() V28() Element of REAL

W is Element of (M)

V9 is ext-real V27() V28() Element of REAL

M is non empty MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

[:(M),(M):] is non empty set

{ b

( b

bool [:(M),(M):] is non empty set

{ b

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

[:(M),(M):] is non empty set

(M) is Element of bool [:(M),(M):]

bool [:(M),(M):] is non empty set

{ b

( b

Z is Element of [:(M),(M):]

V is Element of [:(M),(M):]

Q is Element of (M)

W is Element of (M)

[Q,W] is Element of [:(M),(M):]

V9 is ext-real V27() V28() Element of REAL

V is Element of (M)

Q is Element of (M)

[V,Q] is Element of [:(M),(M):]

W is ext-real V27() V28() Element of REAL

V9 is Element of (M)

Q9 is Element of (M)

[V9,Q9] is Element of [:(M),(M):]

W9 is ext-real V27() V28() Element of REAL

M is non empty MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

[:(M),(M),REAL:] is non empty set

{ b

( b

bool [:(M),(M),REAL:] is non empty set

{ b

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

[:(M),(M),REAL:] is non empty set

(M) is Element of bool [:(M),(M),REAL:]

bool [:(M),(M),REAL:] is non empty set

{ b

( b

Z is Element of [:(M),(M),REAL:]

V is Element of [:(M),(M),REAL:]

Q is Element of (M)

W is Element of (M)

V9 is ext-real V27() V28() Element of REAL

[Q,W,V9] is Element of [:(M),(M),REAL:]

V is Element of (M)

Q is Element of (M)

W is ext-real V27() V28() Element of REAL

[V,Q,W] is Element of [:(M),(M),REAL:]

V9 is Element of (M)

Q9 is Element of (M)

W9 is ext-real V27() V28() Element of REAL

[V9,Q9,W9] is Element of [:(M),(M),REAL:]

M is non empty Reflexive symmetric triangle MetrStruct

(M) is Element of bool (M)

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

bool (M) is non empty set

{ b

for b

(M) is Element of bool (M)

{ b

for b

Z is Element of (M)

V is Element of (M)

Q is ext-real V27() V28() Element of REAL

Z is Element of (M)

V is Element of (M)

Q is ext-real V27() V28() Element of REAL

M is non empty Reflexive symmetric triangle MetrStruct

(M) is Element of bool [:(M),(M),REAL:]

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

[:(M),(M),REAL:] is non empty set

bool [:(M),(M),REAL:] is non empty set

{ b

( b

(M) is Element of bool (M)

bool (M) is non empty set

{ b

for b

(M) is Element of bool (M)

{ b

for b

(M) is V29() V30() V31() Element of bool REAL

{ b

[:(M),(M),(M):] is Element of bool [:(M),(M),REAL:]

Z is Element of [:(M),(M),REAL:]

V is Element of (M)

Q is Element of (M)

W is ext-real V27() V28() Element of REAL

[V,Q,W] is Element of [:(M),(M),REAL:]

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

Z is Element of (M)

V is Element of (M)

Q is ext-real V27() V28() Element of REAL

W is ext-real V27() V28() Element of REAL

V9 is Element of the carrier of M

(M,V9) is Element of bool the carrier of M

{ b

Q9 is Element of the carrier of M

(M,Q9) is Element of bool the carrier of M

{ b

dist (V9,Q9) is ext-real V27() V28() Element of REAL

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

Z is Element of (M)

V is Element of (M)

Q is Element of the carrier of M

(M,Q) is Element of bool the carrier of M

{ b

W is Element of the carrier of M

(M,W) is Element of bool the carrier of M

{ b

dist (Q,W) is ext-real V27() V28() Element of REAL

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

[:(M),(M):] is non empty set

[:[:(M),(M):],REAL:] is non empty set

bool [:[:(M),(M):],REAL:] is non empty set

Z is Element of (M)

V is Element of (M)

Z is V12() V37([:(M),(M):], REAL ) Element of bool [:[:(M),(M):],REAL:]

V is Element of (M)

Q is Element of (M)

Z . (V,Q) is ext-real V27() V28() Element of REAL

W is Element of the carrier of M

V9 is Element of the carrier of M

dist (W,V9) is ext-real V27() V28() Element of REAL

Z is V12() V37([:(M),(M):], REAL ) Element of bool [:[:(M),(M):],REAL:]

V is V12() V37([:(M),(M):], REAL ) Element of bool [:[:(M),(M):],REAL:]

Q is Element of (M)

W is Element of (M)

Z . (Q,W) is ext-real V27() V28() Element of REAL

V . (Q,W) is ext-real V27() V28() Element of REAL

V9 is Element of the carrier of M

(M,V9) is Element of bool the carrier of M

{ b

Q9 is Element of the carrier of M

(M,Q9) is Element of bool the carrier of M

{ b

dist (V9,Q9) is ext-real V27() V28() Element of REAL

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

(M) is V12() V37([:(M),(M):], REAL ) Element of bool [:[:(M),(M):],REAL:]

[:(M),(M):] is non empty set

[:[:(M),(M):],REAL:] is non empty set

bool [:[:(M),(M):],REAL:] is non empty set

Z is Element of (M)

V is Element of (M)

(M) . (Z,V) is ext-real V27() V28() Element of REAL

Q is Element of the carrier of M

(M,Q) is Element of bool the carrier of M

{ b

W is Element of the carrier of M

(M,W) is Element of bool the carrier of M

{ b

dist (Q,W) is ext-real V27() V28() Element of REAL

Q is Element of the carrier of M

(M,Q) is Element of bool the carrier of M

{ b

W is Element of the carrier of M

(M,W) is Element of bool the carrier of M

{ b

dist (Q,W) is ext-real V27() V28() Element of REAL

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

(M) is V12() V37([:(M),(M):], REAL ) Element of bool [:[:(M),(M):],REAL:]

[:(M),(M):] is non empty set

[:[:(M),(M):],REAL:] is non empty set

bool [:[:(M),(M):],REAL:] is non empty set

Z is Element of (M)

V is Element of (M)

(M) . (Z,V) is ext-real V27() V28() Element of REAL

(M) . (V,Z) is ext-real V27() V28() Element of REAL

Q is Element of the carrier of M

(M,Q) is Element of bool the carrier of M

{ b

W is Element of the carrier of M

(M,W) is Element of bool the carrier of M

{ b

dist (W,Q) is ext-real V27() V28() Element of REAL

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

(M) is V12() V37([:(M),(M):], REAL ) Element of bool [:[:(M),(M):],REAL:]

[:(M),(M):] is non empty set

[:[:(M),(M):],REAL:] is non empty set

bool [:[:(M),(M):],REAL:] is non empty set

Z is Element of (M)

Q is Element of (M)

(M) . (Z,Q) is ext-real V27() V28() Element of REAL

V is Element of (M)

(M) . (Z,V) is ext-real V27() V28() Element of REAL

(M) . (V,Q) is ext-real V27() V28() Element of REAL

((M) . (Z,V)) + ((M) . (V,Q)) is ext-real V27() V28() set

W is Element of the carrier of M

(M,W) is Element of bool the carrier of M

{ b

V9 is Element of the carrier of M

(M,V9) is Element of bool the carrier of M

{ b

Q9 is Element of the carrier of M

(M,Q9) is Element of bool the carrier of M

{ b

dist (Q9,V9) is ext-real V27() V28() Element of REAL

dist (W,V9) is ext-real V27() V28() Element of REAL

dist (W,Q9) is ext-real V27() V28() Element of REAL

M is non empty Reflexive symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

(M) is V12() V37([:(M),(M):], REAL ) Element of bool [:[:(M),(M):],REAL:]

[:(M),(M):] is non empty set

[:[:(M),(M):],REAL:] is non empty set

bool [:[:(M),(M):],REAL:] is non empty set

MetrStruct(# (M),(M) #) is strict MetrStruct

the carrier of MetrStruct(# (M),(M) #) is set

V is Element of the carrier of MetrStruct(# (M),(M) #)

Q is Element of the carrier of MetrStruct(# (M),(M) #)

W is Element of the carrier of MetrStruct(# (M),(M) #)

dist (V,Q) is ext-real V27() V28() Element of REAL

V9 is Element of (M)

Q9 is Element of (M)

(M) . (V9,Q9) is ext-real V27() V28() Element of REAL

dist (Q,V) is ext-real V27() V28() Element of REAL

(M) . (Q9,V9) is ext-real V27() V28() Element of REAL

dist (V,W) is ext-real V27() V28() Element of REAL

W9 is Element of (M)

(M) . (V9,W9) is ext-real V27() V28() Element of REAL

dist (Q,W) is ext-real V27() V28() Element of REAL

(M) . (Q9,W9) is ext-real V27() V28() Element of REAL

(dist (V,Q)) + (dist (Q,W)) is ext-real V27() V28() set

M is non empty Reflexive symmetric triangle MetrStruct

(M) is Reflexive discerning symmetric triangle MetrStruct

(M) is non empty set

the carrier of M is non empty set

bool the carrier of M is non empty set

{ b

(M) is V12() V37([:(M),(M):], REAL ) Element of bool [:[:(M),(M):],REAL:]

[:(M),(M):] is non empty set

[:[:(M),(M):],REAL:] is non empty set

bool [:[:(M),(M):],REAL:] is non empty set

MetrStruct(# (M),(M) #) is strict MetrStruct