:: METRIC_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let M be non empty MetrStruct ;
let x, y be Element of M;
pred x tolerates y means :Def1: :: METRIC_2:def 1
dist x,y = 0;
end;

:: deftheorem Def1 defines tolerates METRIC_2:def 1 :
for M being non empty MetrStruct
for x, y being Element of M holds
( x tolerates y iff dist x,y = 0 );

definition
let M be non empty Reflexive MetrStruct ;
let x, y be Element of M;
:: original: tolerates
redefine pred x tolerates y;
reflexivity
for x being Element of M holds x tolerates x
proof end;
end;

definition
let M be non empty symmetric MetrStruct ;
let x, y be Element of M;
:: original: tolerates
redefine pred x tolerates y;
symmetry
for x, y being Element of M st x tolerates y holds
y tolerates x
proof end;
end;

definition
let M be non empty MetrStruct ;
let x be Element of M;
func x -neighbour -> Subset of M equals :: METRIC_2:def 2
{ y where y is Element of M : x tolerates y } ;
coherence
{ y where y is Element of M : x tolerates y } is Subset of M
proof end;
end;

:: deftheorem defines -neighbour METRIC_2:def 2 :
for M being non empty MetrStruct
for x being Element of M holds x -neighbour = { y where y is Element of M : x tolerates y } ;

definition
let M be non empty MetrStruct ;
mode equivalence_class of M -> Subset of M means :Def3: :: METRIC_2:def 3
ex x being Element of M st it = x -neighbour ;
existence
ex b1 being Subset of M ex x being Element of M st b1 = x -neighbour
proof end;
end;

:: deftheorem Def3 defines equivalence_class METRIC_2:def 3 :
for M being non empty MetrStruct
for b2 being Subset of M holds
( b2 is equivalence_class of M iff ex x being Element of M st b2 = x -neighbour );

Lm1: for M being non empty Reflexive MetrStruct
for x being Element of M holds x tolerates x
;

theorem :: METRIC_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: METRIC_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for x, y, z being Element of M st x tolerates y & y tolerates z holds
x tolerates z
proof end;

theorem Th7: :: METRIC_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for x, y being Element of M holds
( y in x -neighbour iff y tolerates x )
proof end;

theorem :: METRIC_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds
p tolerates q
proof end;

theorem Th9: :: METRIC_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for x being Element of M holds x in x -neighbour
proof end;

theorem :: METRIC_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for x, y being Element of M holds
( x in y -neighbour iff y in x -neighbour )
proof end;

theorem :: METRIC_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for p, x, y being Element of M st p in x -neighbour & x tolerates y holds
p in y -neighbour
proof end;

theorem Th12: :: METRIC_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for x, y being Element of M st y in x -neighbour holds
x -neighbour = y -neighbour
proof end;

theorem Th13: :: METRIC_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for x, y being Element of M holds
( x -neighbour = y -neighbour iff x tolerates y )
proof end;

theorem :: METRIC_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for x, y being Element of M holds
( x -neighbour meets y -neighbour iff x tolerates y )
proof end;

theorem :: METRIC_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th16: :: METRIC_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V being equivalence_class of M holds V is non empty set
proof end;

registration
let M be PseudoMetricSpace;
cluster -> non empty equivalence_class of M;
coherence
for b1 being equivalence_class of M holds not b1 is empty
by Th16;
end;

theorem Th17: :: METRIC_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds
dist p,q = 0
proof end;

theorem Th18: :: METRIC_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty Reflexive discerning MetrStruct
for x, y being Element of M holds
( x tolerates y iff x = y )
proof end;

theorem Th19: :: METRIC_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for x, y being Element of M holds
( y in x -neighbour iff y = x )
proof end;

theorem Th20: :: METRIC_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for x being Element of M holds x -neighbour = {x}
proof end;

theorem :: METRIC_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for V being Subset of M holds
( V is equivalence_class of M iff ex x being Element of M st V = {x} )
proof end;

definition
let M be non empty MetrStruct ;
func M -neighbour -> set equals :: METRIC_2:def 4
{ s where s is Subset of M : ex x being Element of M st x -neighbour = s } ;
coherence
{ s where s is Subset of M : ex x being Element of M st x -neighbour = s } is set
;
end;

:: deftheorem defines -neighbour METRIC_2:def 4 :
for M being non empty MetrStruct holds M -neighbour = { s where s is Subset of M : ex x being Element of M st x -neighbour = s } ;

registration
let M be non empty MetrStruct ;
cluster M -neighbour -> non empty ;
coherence
not M -neighbour is empty
proof end;
end;

theorem :: METRIC_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th23: :: METRIC_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for M being non empty MetrStruct holds
( V in M -neighbour iff ex x being Element of M st V = x -neighbour )
proof end;

theorem :: METRIC_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrStruct
for x being Element of M holds x -neighbour in M -neighbour ;

theorem :: METRIC_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th26: :: METRIC_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for M being non empty MetrStruct holds
( V in M -neighbour iff V is equivalence_class of M )
proof end;

theorem :: METRIC_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for x being Element of M holds {x} in M -neighbour
proof end;

theorem :: METRIC_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for M being non empty MetrSpace holds
( V in M -neighbour iff ex x being Element of M st V = {x} )
proof end;

theorem Th29: :: METRIC_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds
dist p1,q1 = dist p2,q2
proof end;

definition
let M be non empty MetrStruct ;
let V, Q be Element of M -neighbour ;
let v be Element of REAL ;
pred V,Q is_dst v means :Def5: :: METRIC_2:def 5
for p, q being Element of M st p in V & q in Q holds
dist p,q = v;
end;

:: deftheorem Def5 defines is_dst METRIC_2:def 5 :
for M being non empty MetrStruct
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( V,Q is_dst v iff for p, q being Element of M st p in V & q in Q holds
dist p,q = v );

theorem :: METRIC_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th31: :: METRIC_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist p,q = v ) )
proof end;

theorem Th32: :: METRIC_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( V,Q is_dst v iff Q,V is_dst v )
proof end;

definition
let M be non empty MetrStruct ;
let V, Q be Element of M -neighbour ;
func ev_eq_1 V,Q -> Subset of REAL equals :: METRIC_2:def 6
{ v where v is Element of REAL : V,Q is_dst v } ;
coherence
{ v where v is Element of REAL : V,Q is_dst v } is Subset of REAL
proof end;
end;

:: deftheorem defines ev_eq_1 METRIC_2:def 6 :
for M being non empty MetrStruct
for V, Q being Element of M -neighbour holds ev_eq_1 V,Q = { v where v is Element of REAL : V,Q is_dst v } ;

theorem :: METRIC_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( v in ev_eq_1 V,Q iff V,Q is_dst v )
proof end;

definition
let M be non empty MetrStruct ;
let v be Element of REAL ;
func ev_eq_2 v,M -> Subset of [:(M -neighbour ),(M -neighbour ):] equals :: METRIC_2:def 7
{ W where W is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v )
}
;
coherence
{ W where W is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v )
}
is Subset of [:(M -neighbour ),(M -neighbour ):]
proof end;
end;

:: deftheorem defines ev_eq_2 METRIC_2:def 7 :
for M being non empty MetrStruct
for v being Element of REAL holds ev_eq_2 v,M = { W where W is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v )
}
;

theorem :: METRIC_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for v being Element of REAL
for W being Element of [:(M -neighbour ),(M -neighbour ):] holds
( W in ev_eq_2 v,M iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
proof end;

definition
let M be non empty MetrStruct ;
func real_in_rel M -> Subset of REAL equals :: METRIC_2:def 8
{ v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v } ;
coherence
{ v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v } is Subset of REAL
proof end;
end;

:: deftheorem defines real_in_rel METRIC_2:def 8 :
for M being non empty MetrStruct holds real_in_rel M = { v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v } ;

theorem :: METRIC_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for v being Element of REAL holds
( v in real_in_rel M iff ex V, Q being Element of M -neighbour st V,Q is_dst v )
proof end;

definition
let M be non empty MetrStruct ;
func elem_in_rel_1 M -> Subset of (M -neighbour ) equals :: METRIC_2:def 9
{ V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } ;
coherence
{ V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } is Subset of (M -neighbour )
proof end;
end;

:: deftheorem defines elem_in_rel_1 METRIC_2:def 9 :
for M being non empty MetrStruct holds elem_in_rel_1 M = { V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } ;

theorem :: METRIC_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th40: :: METRIC_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V being Element of M -neighbour holds
( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
proof end;

definition
let M be non empty MetrStruct ;
func elem_in_rel_2 M -> Subset of (M -neighbour ) equals :: METRIC_2:def 10
{ Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } ;
coherence
{ Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } is Subset of (M -neighbour )
proof end;
end;

:: deftheorem defines elem_in_rel_2 METRIC_2:def 10 :
for M being non empty MetrStruct holds elem_in_rel_2 M = { Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } ;

theorem :: METRIC_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th42: :: METRIC_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for Q being Element of M -neighbour holds
( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
proof end;

definition
let M be non empty MetrStruct ;
func elem_in_rel M -> Subset of [:(M -neighbour ),(M -neighbour ):] equals :: METRIC_2:def 11
{ VQ where VQ is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v )
}
;
coherence
{ VQ where VQ is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v )
}
is Subset of [:(M -neighbour ),(M -neighbour ):]
proof end;
end;

:: deftheorem defines elem_in_rel METRIC_2:def 11 :
for M being non empty MetrStruct holds elem_in_rel M = { VQ where VQ is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v )
}
;

theorem :: METRIC_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for VQ being Element of [:(M -neighbour ),(M -neighbour ):] holds
( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) )
proof end;

definition
let M be non empty MetrStruct ;
func set_in_rel M -> Subset of [:(M -neighbour ),(M -neighbour ),REAL :] equals :: METRIC_2:def 12
{ VQv where VQv is Element of [:(M -neighbour ),(M -neighbour ),REAL :] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v )
}
;
coherence
{ VQv where VQv is Element of [:(M -neighbour ),(M -neighbour ),REAL :] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v )
}
is Subset of [:(M -neighbour ),(M -neighbour ),REAL :]
proof end;
end;

:: deftheorem defines set_in_rel METRIC_2:def 12 :
for M being non empty MetrStruct holds set_in_rel M = { VQv where VQv is Element of [:(M -neighbour ),(M -neighbour ),REAL :] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v )
}
;

theorem :: METRIC_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th46: :: METRIC_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for VQv being Element of [:(M -neighbour ),(M -neighbour ),REAL :] holds
( VQv in set_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) )
proof end;

theorem :: METRIC_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace holds elem_in_rel_1 M = elem_in_rel_2 M
proof end;

theorem :: METRIC_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace holds set_in_rel M c= [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):]
proof end;

theorem :: METRIC_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v1, v2 being Element of REAL st V,Q is_dst v1 & V,Q is_dst v2 holds
v1 = v2
proof end;

theorem :: METRIC_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th52: :: METRIC_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v
proof end;

definition
let M be PseudoMetricSpace;
func nbourdist M -> Function of [:(M -neighbour ),(M -neighbour ):], REAL means :Def13: :: METRIC_2:def 13
for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
it . V,Q = dist p,q;
existence
ex b1 being Function of [:(M -neighbour ),(M -neighbour ):], REAL st
for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b1 . V,Q = dist p,q
proof end;
uniqueness
for b1, b2 being Function of [:(M -neighbour ),(M -neighbour ):], REAL st ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b1 . V,Q = dist p,q ) & ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b2 . V,Q = dist p,q ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines nbourdist METRIC_2:def 13 :
for M being PseudoMetricSpace
for b2 being Function of [:(M -neighbour ),(M -neighbour ):], REAL holds
( b2 = nbourdist M iff for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b2 . V,Q = dist p,q );

theorem :: METRIC_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th54: :: METRIC_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour holds
( (nbourdist M) . V,Q = 0 iff V = Q )
proof end;

theorem Th55: :: METRIC_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour holds (nbourdist M) . V,Q = (nbourdist M) . Q,V
proof end;

theorem Th56: :: METRIC_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being PseudoMetricSpace
for V, Q, W being Element of M -neighbour holds (nbourdist M) . V,W <= ((nbourdist M) . V,Q) + ((nbourdist M) . Q,W)
proof end;

definition
let M be PseudoMetricSpace;
func Eq_classMetricSpace M -> MetrSpace equals :: METRIC_2:def 14
MetrStruct(# (M -neighbour ),(nbourdist M) #);
coherence
MetrStruct(# (M -neighbour ),(nbourdist M) #) is MetrSpace
proof end;
end;

:: deftheorem defines Eq_classMetricSpace METRIC_2:def 14 :
for M being PseudoMetricSpace holds Eq_classMetricSpace M = MetrStruct(# (M -neighbour ),(nbourdist M) #);

registration
let M be PseudoMetricSpace;
cluster Eq_classMetricSpace M -> non empty strict ;
coherence
( Eq_classMetricSpace M is strict & not Eq_classMetricSpace M is empty )
;
end;