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;
consider q being Element of M such that
A2: Q = q -neighbour by Th23;
A3: q in Q by A2, Th9;
A4: p in V by A1, Th9;
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