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 Th23;
A2: p in V by A1, Th9;
consider q being Element of M such that
A3: Q = q -neighbour by Th23;
A4: q in Q by A3, Th9;
then (nbourdist M) . V,Q = dist q,p by A2, Def13
.= (nbourdist M) . Q,V by A2, A4, Def13 ;
hence (nbourdist M) . V,Q = (nbourdist M) . Q,V ; :: thesis: verum