let M be PseudoMetricSpace; :: thesis: 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
let V, Q be Element of M -neighbour ; :: thesis: for v1, v2 being Element of REAL st V,Q is_dst v1 & V,Q is_dst v2 holds
v1 = v2
let v1, v2 be Element of REAL ; :: thesis: ( V,Q is_dst v1 & V,Q is_dst v2 implies v1 = v2 )
assume that
A1: V,Q is_dst v1 and
A2: V,Q is_dst v2 ; :: thesis: v1 = v2
consider p1 being Element of M such that
A3: V = p1 -neighbour by Th15;
consider q1 being Element of M such that
A4: Q = q1 -neighbour by Th15;
A5: q1 in Q by A4, Th4;
A6: p1 in V by A3, Th4;
then dist (p1,q1) = v1 by A1, A5;
hence v1 = v2 by A2, A6, A5; :: thesis: verum