:: METRIC_1 semantic presentation

begin

definition
attr c1 is strict ;
struct MetrStruct -> ( ( ) ( ) 1-sorted ) ;
aggr MetrStruct(# carrier, distance #) -> ( ( strict ) ( strict ) MetrStruct ) ;
sel distance c1 -> ( ( Function-like V18([: the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [: the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([: the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [: the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ;
end;

registration
cluster non empty strict for ( ( ) ( ) MetrStruct ) ;
end;

definition
let A, B be ( ( ) ( ) set ) ;
let f be ( ( Function-like ) ( Relation-like [:A : ( ( ) ( ) set ) ,B : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
let a be ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ;
let b be ( ( ) ( ) Element of B : ( ( ) ( ) set ) ) ;
:: original: .
redefine func f . (a,b) -> ( ( ) ( ext-real V34() real ) Real) ;
end;

definition
let M be ( ( ) ( ) MetrStruct ) ;
let a, b be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
func dist (a,b) -> ( ( ) ( ext-real V34() real ) Real) equals :: METRIC_1:def 1
 the distance of M : ( ( ) ( ) 2-sorted ) : ( ( Function-like V18([: the carrier of M : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [: the carrier of M : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([: the carrier of M : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [: the carrier of M : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) Element of M : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( ext-real V34() real ) Real) ;
end;

notation
synonym Empty^2-to-zero for op2 ;
end;

definition
:: original: Empty^2-to-zero
redefine func Empty^2-to-zero -> ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ;
end;

registration
cluster Empty^2-to-zero : ( ( ) ( ) set ) -> Relation-like Function-like natural-valued for ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
end;

registration
let f be ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) Function) ;
let x, y be ( ( ) ( ) set ) ;
cluster f : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) . (x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> natural ;
end;

definition
let A be ( ( ) ( ) set ) ;
let f be ( ( Function-like ) ( Relation-like [:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
attr f is Reflexive means :: METRIC_1:def 2
 for a being ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) holds f : ( ( ) ( ) set ) . (a : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ;
attr f is discerning means :: METRIC_1:def 3
 for a, b being ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) st f : ( ( ) ( ) set ) . (a : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) = b : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ;
attr f is symmetric means :: METRIC_1:def 4
 for a, b being ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) holds f : ( ( ) ( ) set ) . (a : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = f : ( ( ) ( ) set ) . (b : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) ;
attr f is triangle means :: METRIC_1:def 5
 for a, b, c being ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) holds f : ( ( ) ( ) set ) . (a : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) <= (f : ( ( ) ( ) set ) . (a : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) + (f : ( ( ) ( ) set ) . (b : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ;
end;

definition
let M be ( ( ) ( ) MetrStruct ) ;
attr M is Reflexive means :: METRIC_1:def 6
 the distance of M : ( ( ) ( ) set ) : ( ( Function-like V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) is Reflexive ;
attr M is discerning means :: METRIC_1:def 7
 the distance of M : ( ( ) ( ) set ) : ( ( Function-like V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) is discerning ;
attr M is symmetric means :: METRIC_1:def 8
 the distance of M : ( ( ) ( ) set ) : ( ( Function-like V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) is symmetric ;
attr M is triangle means :: METRIC_1:def 9
 the distance of M : ( ( ) ( ) set ) : ( ( Function-like V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) is triangle ;
end;

registration
cluster non empty strict Reflexive discerning symmetric triangle for ( ( ) ( ) MetrStruct ) ;
end;

definition
mode MetrSpace is ( ( Reflexive discerning symmetric triangle ) ( Reflexive discerning symmetric triangle ) MetrStruct ) ;
end;

theorem :: METRIC_1:1
for M being ( ( ) ( ) MetrStruct ) holds
( ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) iff M : ( ( ) ( ) MetrStruct ) is Reflexive ) ;

theorem :: METRIC_1:2
for M being ( ( ) ( ) MetrStruct ) holds
( ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) iff M : ( ( ) ( ) MetrStruct ) is discerning ) ;

theorem :: METRIC_1:3
for M being ( ( ) ( ) MetrStruct ) st ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = dist (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) ) holds
M : ( ( ) ( ) MetrStruct ) is symmetric ;

theorem :: METRIC_1:4
for M being ( ( ) ( ) MetrStruct ) holds
( ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) <= (dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) + (dist (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) iff M : ( ( ) ( ) MetrStruct ) is triangle ) ;

definition
let M be ( ( symmetric ) ( symmetric ) MetrStruct ) ;
let a, b be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
:: original: dist
redefine func dist (a,b) -> ( ( ) ( ext-real V34() real ) Real) ;
commutativity
for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds dist (a : ( ( symmetric ) ( symmetric ) MetrStruct ) ,b : ( ( symmetric ) ( symmetric ) MetrStruct ) ) : ( ( ) ( ext-real V34() real ) Real) = dist (b : ( ( symmetric ) ( symmetric ) MetrStruct ) ,a : ( ( symmetric ) ( symmetric ) MetrStruct ) ) : ( ( ) ( ext-real V34() real ) Real) ;
end;

theorem :: METRIC_1:5
for M being ( ( Reflexive symmetric triangle ) ( Reflexive symmetric triangle ) MetrStruct )
for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) <= dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) ;

theorem :: METRIC_1:6
for M being ( ( ) ( ) MetrStruct ) st ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( ( dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) implies a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) implies dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) & dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = dist (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) & dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) <= (dist (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) + (dist (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ) holds
M : ( ( ) ( ) MetrStruct ) is ( ( Reflexive discerning symmetric triangle ) ( Reflexive discerning symmetric triangle ) MetrSpace) ;

theorem :: METRIC_1:7
for M being ( ( Reflexive discerning symmetric triangle ) ( Reflexive discerning symmetric triangle ) MetrSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) < dist (x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) ;

definition
let A be ( ( ) ( ) set ) ;
func discrete_dist A -> ( ( Function-like V18([:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) means :: METRIC_1:def 10
 for x, y being ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) holds
( it : ( ( ) ( ) set ) . (x : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) & ( x : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) <> y : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) implies it : ( ( ) ( ) set ) . (x : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) );
end;

definition
let A be ( ( ) ( ) set ) ;
func DiscreteSpace A -> ( ( strict ) ( strict ) MetrStruct ) equals :: METRIC_1:def 11
 MetrStruct(# A : ( ( ) ( ) set ) ,(discrete_dist A : ( ( ) ( ) set ) ) : ( ( Function-like V18([:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) #) : ( ( strict ) ( strict ) MetrStruct ) ;
end;

registration
let A be ( ( non empty ) ( non empty ) set ) ;
cluster DiscreteSpace A : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( strict ) MetrStruct ) -> non empty strict ;
end;

registration
let A be ( ( ) ( ) set ) ;
cluster DiscreteSpace A : ( ( ) ( ) set ) : ( ( strict ) ( strict ) MetrStruct ) -> strict Reflexive discerning symmetric triangle ;
end;

definition
func real_dist -> ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) means :: METRIC_1:def 12
 for x, y being ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) holds it : ( ( ) ( ) set ) . (x : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ,y : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = abs (x : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) - y : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ;
end;

theorem :: METRIC_1:8
for x, y being ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) holds
( real_dist : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ,y : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) iff x : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) = y : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ;

theorem :: METRIC_1:9
for x, y being ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) holds real_dist : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ,y : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = real_dist : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (y : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ,x : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) ;

theorem :: METRIC_1:10
for x, y, z being ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) holds real_dist : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ,y : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) <= (real_dist : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ,z : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) + (real_dist : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (z : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ,y : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ;

definition
func RealSpace -> ( ( strict ) ( strict ) MetrStruct ) equals :: METRIC_1:def 13
 MetrStruct(# REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,real_dist : ( ( Function-like V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) #) : ( ( strict ) ( strict ) MetrStruct ) ;
end;

registration
cluster RealSpace : ( ( strict ) ( strict ) MetrStruct ) -> non empty strict ;
end;

registration
cluster RealSpace : ( ( strict ) ( non empty strict ) MetrStruct ) -> strict Reflexive discerning symmetric triangle ;
end;

definition
let M be ( ( ) ( ) MetrStruct ) ;
let p be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
let r be ( ( real ) ( ext-real V34() real ) number ) ;
func Ball (p,r) -> ( ( ) ( ) Subset of ) means :: METRIC_1:def 14
it : ( ( Function-like V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) ( Relation-like M : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) Element of bool [:M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) = { q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) where q is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : dist (p : ( ( ) ( ) set ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) < r : ( ( ) ( ) set ) } if not M : ( ( ) ( ) set ) is empty
otherwise it : ( ( Function-like V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) ( Relation-like M : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) Element of bool [:M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is empty ;
end;

definition
let M be ( ( ) ( ) MetrStruct ) ;
let p be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
let r be ( ( real ) ( ext-real V34() real ) number ) ;
func cl_Ball (p,r) -> ( ( ) ( ) Subset of ) means :: METRIC_1:def 15
it : ( ( Function-like V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) ( Relation-like M : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) Element of bool [:M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) = { q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) where q is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : dist (p : ( ( ) ( ) set ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) <= r : ( ( ) ( ) set ) } if not M : ( ( ) ( ) set ) is empty
otherwise it : ( ( Function-like V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) ( Relation-like M : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) Element of bool [:M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is empty ;
end;

definition
let M be ( ( ) ( ) MetrStruct ) ;
let p be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
let r be ( ( real ) ( ext-real V34() real ) number ) ;
func Sphere (p,r) -> ( ( ) ( ) Subset of ) means :: METRIC_1:def 16
it : ( ( Function-like V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) ( Relation-like M : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) Element of bool [:M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) = { q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) where q is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : dist (p : ( ( ) ( ) set ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = r : ( ( ) ( ) set ) } if not M : ( ( ) ( ) set ) is empty
otherwise it : ( ( Function-like V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) ( Relation-like M : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) ) ) Element of bool [:M : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is empty ;
end;

theorem :: METRIC_1:11
for r being ( ( real ) ( ext-real V34() real ) number )
for M being ( ( ) ( ) MetrStruct )
for p, x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in Ball (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) iff ( not M : ( ( ) ( ) MetrStruct ) is empty & dist (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) < r : ( ( real ) ( ext-real V34() real ) number ) ) ) ;

theorem :: METRIC_1:12
for r being ( ( real ) ( ext-real V34() real ) number )
for M being ( ( ) ( ) MetrStruct )
for p, x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in cl_Ball (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) iff ( not M : ( ( ) ( ) MetrStruct ) is empty & dist (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) <= r : ( ( real ) ( ext-real V34() real ) number ) ) ) ;

theorem :: METRIC_1:13
for r being ( ( real ) ( ext-real V34() real ) number )
for M being ( ( ) ( ) MetrStruct )
for p, x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in Sphere (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) iff ( not M : ( ( ) ( ) MetrStruct ) is empty & dist (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = r : ( ( real ) ( ext-real V34() real ) number ) ) ) ;

theorem :: METRIC_1:14
for r being ( ( real ) ( ext-real V34() real ) number )
for M being ( ( ) ( ) MetrStruct )
for p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds Ball (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) c= cl_Ball (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) ;

theorem :: METRIC_1:15
for r being ( ( real ) ( ext-real V34() real ) number )
for M being ( ( ) ( ) MetrStruct )
for p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds Sphere (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) c= cl_Ball (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) ;

theorem :: METRIC_1:16
for r being ( ( real ) ( ext-real V34() real ) number )
for M being ( ( ) ( ) MetrStruct )
for p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (Sphere (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) )) : ( ( ) ( ) Subset of ) \/ (Ball (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) )) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b2 : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = cl_Ball (p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) ;

theorem :: METRIC_1:17
for r being ( ( real ) ( ext-real V34() real ) number )
for M being ( ( non empty ) ( non empty ) MetrStruct )
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Ball (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) = { q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where q is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : dist (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) < r : ( ( real ) ( ext-real V34() real ) number ) } ;

theorem :: METRIC_1:18
for r being ( ( real ) ( ext-real V34() real ) number )
for M being ( ( non empty ) ( non empty ) MetrStruct )
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds cl_Ball (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) = { q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where q is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : dist (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) <= r : ( ( real ) ( ext-real V34() real ) number ) } ;

theorem :: METRIC_1:19
for r being ( ( real ) ( ext-real V34() real ) number )
for M being ( ( non empty ) ( non empty ) MetrStruct )
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Sphere (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( real ) ( ext-real V34() real ) number ) ) : ( ( ) ( ) Subset of ) = { q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where q is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : dist (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = r : ( ( real ) ( ext-real V34() real ) number ) } ;

begin

theorem :: METRIC_1:20
for x being ( ( ) ( ) set ) holds Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ext-real natural V34() real ) set ) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: METRIC_1:21
for x, y being ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) st x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) <> y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) holds
0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) < Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( ext-real natural V34() real ) Real) ;

theorem :: METRIC_1:22
for x, y being ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) holds Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( ext-real natural V34() real ) Real) = Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( ext-real natural V34() real ) Real) ;

theorem :: METRIC_1:23
for x, y, z being ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) holds Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,z : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( ext-real natural V34() real ) Real) <= (Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) )) : ( ( ) ( ext-real natural V34() real ) Real) + (Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,z : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) )) : ( ( ) ( ext-real natural V34() real ) Real) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ;

theorem :: METRIC_1:24
for x, y, z being ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) holds Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,z : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( ext-real natural V34() real ) Real) <= max ((Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) )) : ( ( ) ( ext-real natural V34() real ) Real) ,(Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,z : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) )) : ( ( ) ( ext-real natural V34() real ) Real) ) : ( ( ) ( ext-real V34() real ) set ) ;

definition
let A be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ;
attr f is Discerning means :: METRIC_1:def 17
 for a, b being ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) holds
0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) < f : ( ( ) ( ) set ) . (a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) ;
end;

definition
let M be ( ( non empty ) ( non empty ) MetrStruct ) ;
attr M is Discerning means :: METRIC_1:def 18
 the distance of M : ( ( ) ( ) set ) : ( ( Function-like V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [: the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) is Discerning ;
end;

theorem :: METRIC_1:25
for M being ( ( non empty ) ( non empty ) MetrStruct ) holds
( ( for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) < dist (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) ) iff M : ( ( non empty ) ( non empty ) MetrStruct ) is Discerning ) ;

registration
cluster MetrStruct(# 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) #) : ( ( strict ) ( strict ) MetrStruct ) -> non empty strict ;
end;

registration
cluster MetrStruct(# 1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,Empty^2-to-zero : ( ( Function-like V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like total V18([:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Function of [:1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) #) : ( ( strict ) ( non empty strict ) MetrStruct ) -> strict Reflexive symmetric triangle Discerning ;
end;

definition
let M be ( ( non empty ) ( non empty ) MetrStruct ) ;
attr M is ultra means :: METRIC_1:def 19
 for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds dist (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) <= max ((dist (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) ,(dist (b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) ) : ( ( ) ( ext-real V34() real ) set ) ;
end;

registration
cluster non empty strict Reflexive symmetric triangle Discerning ultra for ( ( ) ( ) MetrStruct ) ;
end;

theorem :: METRIC_1:26
for M being ( ( non empty Reflexive Discerning ) ( non empty Reflexive Discerning ) MetrStruct )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) <= dist (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) ;

definition
mode PseudoMetricSpace is ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) ;
mode SemiMetricSpace is ( ( non empty Reflexive symmetric Discerning ) ( non empty Reflexive symmetric Discerning ) MetrStruct ) ;
mode NonSymmetricMetricSpace is ( ( non empty Reflexive triangle Discerning ) ( non empty Reflexive triangle Discerning ) MetrStruct ) ;
mode UltraMetricSpace is ( ( non empty Reflexive symmetric Discerning ultra ) ( non empty Reflexive symmetric Discerning ultra ) MetrStruct ) ;
end;

registration
cluster non empty Reflexive discerning symmetric triangle -> non empty Reflexive discerning symmetric triangle Discerning for ( ( ) ( ) MetrStruct ) ;
end;

registration
cluster non empty Reflexive symmetric Discerning ultra -> non empty Reflexive discerning symmetric triangle Discerning ultra for ( ( ) ( ) MetrStruct ) ;
end;

definition
func Set_to_zero -> ( ( Function-like V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) equals :: METRIC_1:def 20
[:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) --> 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued Function-like total V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued natural-valued ) Element of bool [:[:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) ,REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: METRIC_1:27
for x, y being ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) holds Set_to_zero : ( ( Function-like V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( ext-real V34() real ) Real) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: METRIC_1:28
for x, y being ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) holds Set_to_zero : ( ( Function-like V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( ext-real V34() real ) Real) = Set_to_zero : ( ( Function-like V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( ext-real V34() real ) Real) ;

theorem :: METRIC_1:29
for x, y, z being ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) holds Set_to_zero : ( ( Function-like V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,z : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ) : ( ( ) ( ext-real V34() real ) Real) <= (Set_to_zero : ( ( Function-like V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (x : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) )) : ( ( ) ( ext-real V34() real ) Real) + (Set_to_zero : ( ( Function-like V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) . (y : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) ,z : ( ( ) ( ext-real natural V34() real V59() V60() ) Element of 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ) )) : ( ( ) ( ext-real V34() real ) Real) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ;

definition
func ZeroSpace -> ( ( ) ( ) MetrStruct ) equals :: METRIC_1:def 21
 MetrStruct(# 2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,Set_to_zero : ( ( Function-like V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) ) ( Relation-like [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) -defined REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) -valued Function-like total V18([:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) complex-valued ext-real-valued real-valued ) Function of [:2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) ,2 : ( ( ) ( non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( V71() V72() V73() V74() V75() V76() V77() ) Element of bool REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( non empty V36() V71() V72() V73() V74() V77() ) set ) -valued INT : ( ( ) ( non empty V36() V71() V72() V73() V74() V75() V77() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) , REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) #) : ( ( strict ) ( strict ) MetrStruct ) ;
end;

registration
cluster ZeroSpace : ( ( ) ( ) MetrStruct ) -> non empty strict ;
end;

registration
cluster ZeroSpace : ( ( ) ( non empty strict ) MetrStruct ) -> Reflexive symmetric triangle ;
end;

definition
let S be ( ( ) ( ) MetrStruct ) ;
let p, q, r be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
pred q is_between p,r means :: METRIC_1:def 22
( p : ( ( ) ( ) set ) <> q : ( ( ) ( ) set ) & p : ( ( ) ( ) set ) <> r : ( ( Function-like V18(S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) ) ) ( Relation-like S : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) ) ) Element of bool [:S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) & q : ( ( ) ( ) set ) <> r : ( ( Function-like V18(S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) ) ) ( Relation-like S : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) ) ) Element of bool [:S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) & dist (p : ( ( ) ( ) set ) ,r : ( ( Function-like V18(S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) ) ) ( Relation-like S : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) ) ) Element of bool [:S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V34() real ) Real) = (dist (p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) : ( ( ) ( ext-real V34() real ) Real) + (dist (q : ( ( ) ( ) set ) ,r : ( ( Function-like V18(S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) ) ) ( Relation-like S : ( ( ) ( ) set ) -defined K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) -valued Function-like non empty total V18(S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) ) ) Element of bool [:S : ( ( ) ( ) set ) ,K78(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) M4(p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) )) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) )) : ( ( ) ( ext-real V34() real ) Real) : ( ( ) ( ext-real V34() real ) Element of REAL : ( ( ) ( non empty V36() V71() V72() V73() V77() ) set ) ) );
end;

theorem :: METRIC_1:30
for S being ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct )
for p, q, r being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_between p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_between r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: METRIC_1:31
for S being ( ( Reflexive discerning symmetric triangle ) ( Reflexive discerning symmetric triangle ) MetrSpace)
for p, q, r being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_between p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( not p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_between q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_between p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ;

theorem :: METRIC_1:32
for S being ( ( Reflexive discerning symmetric triangle ) ( Reflexive discerning symmetric triangle ) MetrSpace)
for p, q, r, s being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_between p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_between p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_between p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_between q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ;

definition
let M be ( ( non empty ) ( non empty ) MetrStruct ) ;
let p, r be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func open_dist_Segment (p,r) -> ( ( ) ( ) Subset of ) equals :: METRIC_1:def 23
 { q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where q is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_between p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) } ;
end;

theorem :: METRIC_1:33
for M being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace)
for p, r, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in open_dist_Segment (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_between p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

definition
let M be ( ( non empty ) ( non empty ) MetrStruct ) ;
let p, r be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func close_dist_Segment (p,r) -> ( ( ) ( ) Subset of ) equals :: METRIC_1:def 24
 { q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where q is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_between p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) } \/ {p : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ;
end;

theorem :: METRIC_1:34
for M being ( ( non empty ) ( non empty ) MetrStruct )
for p, r, x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in close_dist_Segment (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) iff ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_between p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;