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 A1: ( V,Q is_dst v1 & V,Q is_dst v2 ) ; :: thesis: v1 = v2
consider p1 being Element of M such that
A2: V = p1 -neighbour by Th23;
A3: p1 in V by A2, Th9;
consider q1 being Element of M such that
A4: Q = q1 -neighbour by Th23;
A5: q1 in Q by A4, Th9;
then dist p1,q1 = v1 by A1, A3, Def5;
hence v1 = v2 by A1, A3, A5, Def5; :: thesis: verum