let M be PseudoMetricSpace; :: thesis: for V, Q being Element of M -neighbour holds
( (nbourdist M) . (V,Q) = 0 iff V = Q )
let V, Q be Element of M -neighbour ; :: thesis: ( (nbourdist M) . (V,Q) = 0 iff V = Q )
A1: ( V = Q implies (nbourdist M) . (V,Q) = 0 )

proof

consider p being Element of M such that
A2: V = p -neighbour by Th15;
A3: p in V by A2, Th4;
consider q being Element of M such that
A4: Q = q -neighbour by Th15;
assume V = Q ; :: thesis: (nbourdist M) . (V,Q) = 0
then A5: p tolerates q by A3, A4, Th2;
q in Q by A4, Th4;
then (nbourdist M) . (V,Q) = dist (p,q) by A3, Def13
.= 0 by A5 ;
hence (nbourdist M) . (V,Q) = 0 ; :: thesis: verum

end;

( (nbourdist M) . (V,Q) = 0 implies V = Q )

proof

assume A6: (nbourdist M) . (V,Q) = 0 ; :: thesis: V = Q
consider p being Element of M such that
A7: V = p -neighbour by Th15;
consider q being Element of M such that
A8: Q = q -neighbour by Th15;
A9: q in Q by A8, Th4;
p in V by A7, Th4;
then dist (p,q) = 0 by A6, A9, Def13;
then p tolerates q ;
hence V = Q by A7, A8, Th8; :: thesis: verum

end;

hence ( (nbourdist M) . (V,Q) = 0 iff V = Q ) by A1; :: thesis: verum