:: 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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
bool the carrier of M is non empty set
{ b₁ where b₁ is Element of the carrier of M : S₁[b₁] } 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
{ b₁ where b₁ is Element of the carrier of M : (M, the Element of the carrier of M,b₁) } is set
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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
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₁ where b₁ is Element of the carrier of M : (M,V,b₁) } is set
(M,Z) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
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₁ where b₁ is Element of the carrier of M : (M,V,b₁) } is set
Q is Element of the carrier of M
(M,Q) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,Q,b₁) } is 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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
(M,V) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,V,b₁) } is set
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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
V is Element of the carrier of M
(M,V) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,V,b₁) } is set
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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
V is Element of the carrier of M
(M,V) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,V,b₁) } 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
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₁ where b₁ is Element of the carrier of M : (M,V,b₁) } is set
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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } 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
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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
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₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } 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
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₁ where b₁ is Element of the carrier of M : (M,V,b₁) } 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
{ b₁ where b₁ is Element of the carrier of M : (M,V,b₁) } 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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M, the Element of the carrier of M,b₁) } 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
{ b₁ where b₁ is Element of bool the carrier of Z : ex b₂ being Element of the carrier of Z st (Z,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of Z : (Z,Q,b₁) } is set
V is Element of the carrier of Z
(Z,V) is Element of bool the carrier of Z
{ b₁ where b₁ is Element of the carrier of Z : (Z,V,b₁) } is set
Q is Element of the carrier of Z
(Z,Q) is Element of bool the carrier of Z
{ b₁ where b₁ is Element of the carrier of Z : (Z,Q,b₁) } 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
{ b₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
(M) is non empty set
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of bool the carrier of Z : ex b₂ being Element of the carrier of Z st (Z,b₂) = b₁ } is set
V is Element of the carrier of Z
(Z,V) is Element of bool the carrier of Z
{ b₁ where b₁ is Element of the carrier of Z : (Z,V,b₁) } is set
V is Element of the carrier of Z
(Z,V) is Element of bool the carrier of Z
{ b₁ where b₁ is Element of the carrier of Z : (Z,V,b₁) } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M,Z,b₁) } is set
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₁ where b₁ is Element of bool the carrier of Z : ex b₂ being Element of the carrier of Z st (Z,b₂) = b₁ } is set
V is Element of the carrier of Z
(Z,V) is Element of bool the carrier of Z
{ b₁ where b₁ is Element of the carrier of Z : (Z,V,b₁) } 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
{ b₁ where b₁ is Element of the carrier of Z : (Z,V,b₁) } 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 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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M,W9,b₁) } 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
{ b₁ where b₁ is Element of the carrier of M : (M,W9,b₁) } 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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M,W,b₁) } is set
V9 is Element of the carrier of M
(M,V9) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,V9,b₁) } 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 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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
Z is Element of (M)
V is Element of (M)
{ b₁ where b₁ is ext-real V27() V28() Element of REAL : (M,Z,V,b₁) } is set
{ b₁ where b₁ is ext-real V27() V28() Element of REAL : S₁[b₁] } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
Z is Element of (M)
V is Element of (M)
(M,Z,V) is V29() V30() V31() Element of bool REAL
{ b₁ where b₁ is ext-real V27() V28() Element of REAL : (M,Z,V,b₁) } 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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
[:(M),(M):] is non empty set
Z is ext-real V27() V28() Element of REAL
{ b₁ where b₁ is Element of [:(M),(M):] : ex b₂, b₃ being Element of (M) st
( b₁ = [b₂,b₃] & (M,b₂,b₃,Z) ) } is set
bool [:(M),(M):] is non empty set
{ b₁ where b₁ is Element of [:(M),(M):] : S₁[b₁] } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of [:(M),(M):] : ex b₂, b₃ being Element of (M) st
( b₁ = [b₂,b₃] & (M,b₂,b₃,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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
{ b₁ where b₁ is ext-real V27() V28() Element of REAL : not for b₂, b₃ being Element of (M) holds (M,b₂,b₃,b₁) } is set
{ b₁ where b₁ is ext-real V27() V28() Element of REAL : S₁[b₁] } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
{ b₁ where b₁ is ext-real V27() V28() Element of REAL : not for b₂, b₃ being Element of (M) holds (M,b₂,b₃,b₁) } 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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
{ b₁ where b₁ is Element of (M) : not for b₂ being Element of (M)
for b₃ being ext-real V27() V28() Element of REAL holds (M,b₁,b₂,b₃) } is set
bool (M) is non empty set
{ b₁ where b₁ is Element of (M) : S₁[b₁] } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
(M) is Element of bool (M)
bool (M) is non empty set
{ b₁ where b₁ is Element of (M) : not for b₂ being Element of (M)
for b₃ being ext-real V27() V28() Element of REAL holds (M,b₁,b₂,b₃) } 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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
{ b₁ where b₁ is Element of (M) : not for b₂ being Element of (M)
for b₃ being ext-real V27() V28() Element of REAL holds (M,b₂,b₁,b₃) } is set
bool (M) is non empty set
{ b₁ where b₁ is Element of (M) : S₁[b₁] } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
(M) is Element of bool (M)
bool (M) is non empty set
{ b₁ where b₁ is Element of (M) : not for b₂ being Element of (M)
for b₃ being ext-real V27() V28() Element of REAL holds (M,b₂,b₁,b₃) } 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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
[:(M),(M):] is non empty set
{ b₁ where b₁ is Element of [:(M),(M):] : ex b₂, b₃ being Element of (M) ex b₄ being ext-real V27() V28() Element of REAL st
( b₁ = [b₂,b₃] & (M,b₂,b₃,b₄) ) } is set
bool [:(M),(M):] is non empty set
{ b₁ where b₁ is Element of [:(M),(M):] : S₁[b₁] } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
[:(M),(M):] is non empty set
(M) is Element of bool [:(M),(M):]
bool [:(M),(M):] is non empty set
{ b₁ where b₁ is Element of [:(M),(M):] : ex b₂, b₃ being Element of (M) ex b₄ being ext-real V27() V28() Element of REAL st
( b₁ = [b₂,b₃] & (M,b₂,b₃,b₄) ) } 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
{ b₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
[:(M),(M),REAL:] is non empty set
{ b₁ where b₁ is Element of [:(M),(M),REAL:] : ex b₂, b₃ being Element of (M) ex b₄ being ext-real V27() V28() Element of REAL st
( b₁ = [b₂,b₃,b₄] & (M,b₂,b₃,b₄) ) } is set
bool [:(M),(M),REAL:] is non empty set
{ b₁ where b₁ is Element of [:(M),(M),REAL:] : S₁[b₁] } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of [:(M),(M),REAL:] : ex b₂, b₃ being Element of (M) ex b₄ being ext-real V27() V28() Element of REAL st
( b₁ = [b₂,b₃,b₄] & (M,b₂,b₃,b₄) ) } 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 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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
bool (M) is non empty set
{ b₁ where b₁ is Element of (M) : not for b₂ being Element of (M)
for b₃ being ext-real V27() V28() Element of REAL holds (M,b₁,b₂,b₃) } is set
(M) is Element of bool (M)
{ b₁ where b₁ is Element of (M) : not for b₂ being Element of (M)
for b₃ being ext-real V27() V28() Element of REAL holds (M,b₂,b₁,b₃) } 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 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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } is set
[:(M),(M),REAL:] is non empty set
bool [:(M),(M),REAL:] is non empty set
{ b₁ where b₁ is Element of [:(M),(M),REAL:] : ex b₂, b₃ being Element of (M) ex b₄ being ext-real V27() V28() Element of REAL st
( b₁ = [b₂,b₃,b₄] & (M,b₂,b₃,b₄) ) } is set
(M) is Element of bool (M)
bool (M) is non empty set
{ b₁ where b₁ is Element of (M) : not for b₂ being Element of (M)
for b₃ being ext-real V27() V28() Element of REAL holds (M,b₁,b₂,b₃) } is set
(M) is Element of bool (M)
{ b₁ where b₁ is Element of (M) : not for b₂ being Element of (M)
for b₃ being ext-real V27() V28() Element of REAL holds (M,b₂,b₁,b₃) } is set
(M) is V29() V30() V31() Element of bool REAL
{ b₁ where b₁ is ext-real V27() V28() Element of REAL : not for b₂, b₃ being Element of (M) holds (M,b₂,b₃,b₁) } 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 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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M,V9,b₁) } is set
Q9 is Element of the carrier of M
(M,Q9) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,Q9,b₁) } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M,Q,b₁) } is set
W is Element of the carrier of M
(M,W) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,W,b₁) } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M,V9,b₁) } is set
Q9 is Element of the carrier of M
(M,Q9) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,Q9,b₁) } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M,Q,b₁) } is set
W is Element of the carrier of M
(M,W) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,W,b₁) } 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
{ b₁ where b₁ is Element of the carrier of M : (M,Q,b₁) } is set
W is Element of the carrier of M
(M,W) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,W,b₁) } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M,Q,b₁) } is set
W is Element of the carrier of M
(M,W) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,W,b₁) } is set
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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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
{ b₁ where b₁ is Element of the carrier of M : (M,W,b₁) } is set
V9 is Element of the carrier of M
(M,V9) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,V9,b₁) } is set
Q9 is Element of the carrier of M
(M,Q9) is Element of bool the carrier of M
{ b₁ where b₁ is Element of the carrier of M : (M,Q9,b₁) } 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 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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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 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₁ where b₁ is Element of bool the carrier of M : ex b₂ being Element of the carrier of M st (M,b₂) = b₁ } 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