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: ( (nbourdist M) . V,Q = 0 implies V = Q )

proof

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

end;

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

proof

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

end;

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