let M be PseudoMetricSpace; :: thesis: for V, Q being Element of M -neighbour holds (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V)
let V, Q be Element of M -neighbour ; :: thesis: (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V)
consider p being Element of M such that
A1: V = p -neighbour by Th15;
consider q being Element of M such that
A2: Q = q -neighbour by Th15;
A3: q in Q by A2, Th4;
A4: p in V by A1, Th4;
then (nbourdist M) . (V,Q) = dist (q,p) by A3, Def13
.= (nbourdist M) . (Q,V) by A4, A3, Def13 ;
hence (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V) ; :: thesis: verum