:: 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
is non empty set
is non empty set
bool 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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
bool the carrier of M is non empty set
{ b1 where b1 is Element of the carrier of M : S1[b1] } is set
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
{ b1 where b1 is Element of the carrier of M : (M, the Element of the carrier of M,b1) } is set
M is non empty Reflexive MetrStruct
the carrier of M is non empty set
Z is Element of the carrier of M

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

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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
Q is Element of the carrier of M

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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
Q is Element of the carrier of M

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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set

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
{ b1 where b1 is Element of the carrier of M : (M,V,b1) } is set
(M,Z) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set

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
{ b1 where b1 is Element of the carrier of M : (M,V,b1) } is set
Q is Element of the carrier of M
(M,Q) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,Q,b1) } is set

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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
(M,V) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,V,b1) } is set
Q is Element of the carrier of M
Q is Element of the carrier of M

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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
V is Element of the carrier of M
(M,V) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,V,b1) } is set

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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
V is Element of the carrier of M
(M,V) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,V,b1) } is set
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

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
{ b1 where b1 is Element of the carrier of M : (M,V,b1) } is set

Z is (M)

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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
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

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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
Q is Element of the carrier of M

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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
{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

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
{ b1 where b1 is Element of the carrier of M : (M,V,b1) } is set
{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
{ b1 where b1 is Element of the carrier of M : (M,V,b1) } is set
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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is 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
{ b1 where b1 is Element of the carrier of M : (M, the Element of the carrier of M,b1) } is set
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
{ b1 where b1 is Element of bool the carrier of Z : ex b2 being Element of the carrier of Z st (Z,b2) = b1 } is set
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
{ b1 where b1 is Element of the carrier of Z : (Z,Q,b1) } is set
V is Element of the carrier of Z
(Z,V) is Element of bool the carrier of Z
{ b1 where b1 is Element of the carrier of Z : (Z,V,b1) } is set
Q is Element of the carrier of Z
(Z,Q) is Element of bool the carrier of Z
{ b1 where b1 is Element of the carrier of Z : (Z,Q,b1) } is set
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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
(M) is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
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
{ b1 where b1 is Element of bool the carrier of Z : ex b2 being Element of the carrier of Z st (Z,b2) = b1 } is set
V is Element of the carrier of Z
(Z,V) is Element of bool the carrier of Z
{ b1 where b1 is Element of the carrier of Z : (Z,V,b1) } is set
V is Element of the carrier of Z
(Z,V) is Element of bool the carrier of Z
{ b1 where b1 is Element of the carrier of Z : (Z,V,b1) } is set

the carrier of M is non empty set
(M) is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
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
{ b1 where b1 is Element of the carrier of M : (M,Z,b1) } is set
M is set

(Z) is non empty set
the carrier of Z is non empty set
bool the carrier of Z is non empty set
{ b1 where b1 is Element of bool the carrier of Z : ex b2 being Element of the carrier of Z st (Z,b2) = b1 } is set
V is Element of the carrier of Z
(Z,V) is Element of bool the carrier of Z
{ b1 where b1 is Element of the carrier of Z : (Z,V,b1) } is set
{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
{ b1 where b1 is Element of the carrier of Z : (Z,V,b1) } is set
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 set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
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
{ b1 where b1 is Element of the carrier of M : (M,W9,b1) } is set
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
{ b1 where b1 is Element of the carrier of M : (M,W9,b1) } is set
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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
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
{ b1 where b1 is Element of the carrier of M : (M,W,b1) } is set
V9 is Element of the carrier of M
(M,V9) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,V9,b1) } is set
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 set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
Z is Element of (M)
V is Element of (M)
{ b1 where b1 is ext-real V27() V28() Element of REAL : (M,Z,V,b1) } is set
{ b1 where b1 is ext-real V27() V28() Element of REAL : S1[b1] } is set

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
Z is Element of (M)
V is Element of (M)
(M,Z,V) is V29() V30() V31() Element of bool REAL
{ b1 where b1 is ext-real V27() V28() Element of REAL : (M,Z,V,b1) } is set
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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
[:(M),(M):] is non empty set
Z is ext-real V27() V28() Element of REAL
{ b1 where b1 is Element of [:(M),(M):] : ex b2, b3 being Element of (M) st
( b1 = [b2,b3] & (M,b2,b3,Z) )
}
is set

bool [:(M),(M):] is non empty set
{ b1 where b1 is Element of [:(M),(M):] : S1[b1] } is set

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
[:(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
{ b1 where b1 is Element of [:(M),(M):] : ex b2, b3 being Element of (M) st
( b1 = [b2,b3] & (M,b2,b3,Z) )
}
is set

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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
{ b1 where b1 is ext-real V27() V28() Element of REAL : not for b2, b3 being Element of (M) holds (M,b2,b3,b1) } is set
{ b1 where b1 is ext-real V27() V28() Element of REAL : S1[b1] } is set

(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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
{ b1 where b1 is ext-real V27() V28() Element of REAL : not for b2, b3 being Element of (M) holds (M,b2,b3,b1) } is set
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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
{ b1 where b1 is Element of (M) : not for b2 being Element of (M)
for b3 being ext-real V27() V28() Element of REAL holds (M,b1,b2,b3)
}
is set

bool (M) is non empty set
{ b1 where b1 is Element of (M) : S1[b1] } is set

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
(M) is Element of bool (M)
bool (M) is non empty set
{ b1 where b1 is Element of (M) : not for b2 being Element of (M)
for b3 being ext-real V27() V28() Element of REAL holds (M,b1,b2,b3)
}
is set

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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
{ b1 where b1 is Element of (M) : not for b2 being Element of (M)
for b3 being ext-real V27() V28() Element of REAL holds (M,b2,b1,b3)
}
is set

bool (M) is non empty set
{ b1 where b1 is Element of (M) : S1[b1] } is set

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
(M) is Element of bool (M)
bool (M) is non empty set
{ b1 where b1 is Element of (M) : not for b2 being Element of (M)
for b3 being ext-real V27() V28() Element of REAL holds (M,b2,b1,b3)
}
is set

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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
[:(M),(M):] is non empty set
{ b1 where b1 is Element of [:(M),(M):] : ex b2, b3 being Element of (M) ex b4 being ext-real V27() V28() Element of REAL st
( b1 = [b2,b3] & (M,b2,b3,b4) )
}
is set

bool [:(M),(M):] is non empty set
{ b1 where b1 is Element of [:(M),(M):] : S1[b1] } is set

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
[:(M),(M):] is non empty set
(M) is Element of bool [:(M),(M):]
bool [:(M),(M):] is non empty set
{ b1 where b1 is Element of [:(M),(M):] : ex b2, b3 being Element of (M) ex b4 being ext-real V27() V28() Element of REAL st
( b1 = [b2,b3] & (M,b2,b3,b4) )
}
is set

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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
[:(M),(M),REAL:] is non empty set
{ b1 where b1 is Element of [:(M),(M),REAL:] : ex b2, b3 being Element of (M) ex b4 being ext-real V27() V28() Element of REAL st
( b1 = [b2,b3,b4] & (M,b2,b3,b4) )
}
is set

bool [:(M),(M),REAL:] is non empty set
{ b1 where b1 is Element of [:(M),(M),REAL:] : S1[b1] } is set

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
[:(M),(M),REAL:] is non empty set
(M) is Element of bool [:(M),(M),REAL:]
bool [:(M),(M),REAL:] is non empty set
{ b1 where b1 is Element of [:(M),(M),REAL:] : ex b2, b3 being Element of (M) ex b4 being ext-real V27() V28() Element of REAL st
( b1 = [b2,b3,b4] & (M,b2,b3,b4) )
}
is set

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 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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
bool (M) is non empty set
{ b1 where b1 is Element of (M) : not for b2 being Element of (M)
for b3 being ext-real V27() V28() Element of REAL holds (M,b1,b2,b3)
}
is set

(M) is Element of bool (M)
{ b1 where b1 is Element of (M) : not for b2 being Element of (M)
for b3 being ext-real V27() V28() Element of REAL holds (M,b2,b1,b3)
}
is set

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 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
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
[:(M),(M),REAL:] is non empty set
bool [:(M),(M),REAL:] is non empty set
{ b1 where b1 is Element of [:(M),(M),REAL:] : ex b2, b3 being Element of (M) ex b4 being ext-real V27() V28() Element of REAL st
( b1 = [b2,b3,b4] & (M,b2,b3,b4) )
}
is set

(M) is Element of bool (M)
bool (M) is non empty set
{ b1 where b1 is Element of (M) : not for b2 being Element of (M)
for b3 being ext-real V27() V28() Element of REAL holds (M,b1,b2,b3)
}
is set

(M) is Element of bool (M)
{ b1 where b1 is Element of (M) : not for b2 being Element of (M)
for b3 being ext-real V27() V28() Element of REAL holds (M,b2,b1,b3)
}
is set

(M) is V29() V30() V31() Element of bool REAL
{ b1 where b1 is ext-real V27() V28() Element of REAL : not for b2, b3 being Element of (M) holds (M,b2,b3,b1) } is set
[:(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 set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
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
{ b1 where b1 is Element of the carrier of M : (M,V9,b1) } is set
Q9 is Element of the carrier of M
(M,Q9) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,Q9,b1) } is set
dist (V9,Q9) is ext-real V27() V28() Element of REAL

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
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
{ b1 where b1 is Element of the carrier of M : (M,Q,b1) } is set
W is Element of the carrier of M
(M,W) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,W,b1) } is set
dist (Q,W) is ext-real V27() V28() Element of REAL

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
[:(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
{ b1 where b1 is Element of the carrier of M : (M,V9,b1) } is set
Q9 is Element of the carrier of M
(M,Q9) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,Q9,b1) } is set
dist (V9,Q9) is ext-real V27() V28() Element of REAL

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
(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
{ b1 where b1 is Element of the carrier of M : (M,Q,b1) } is set
W is Element of the carrier of M
(M,W) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,W,b1) } is set
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
{ b1 where b1 is Element of the carrier of M : (M,Q,b1) } is set
W is Element of the carrier of M
(M,W) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,W,b1) } is set
dist (Q,W) is ext-real V27() V28() Element of REAL

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
(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
{ b1 where b1 is Element of the carrier of M : (M,Q,b1) } is set
W is Element of the carrier of M
(M,W) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,W,b1) } is set
dist (W,Q) is ext-real V27() V28() Element of REAL

(M) is non empty set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
(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
{ b1 where b1 is Element of the carrier of M : (M,W,b1) } is set
V9 is Element of the carrier of M
(M,V9) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,V9,b1) } is set
Q9 is Element of the carrier of M
(M,Q9) is Element of bool the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,Q9,b1) } is set
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 set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
(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 set
the carrier of M is non empty set
bool the carrier of M is non empty set
{ b1 where b1 is Element of bool the carrier of M : ex b2 being Element of the carrier of M st (M,b2) = b1 } is set
(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