let M be PseudoMetricSpace; :: thesis: for V, Q, W being Element of M -neighbour holds (nbourdist M) . V,W <= ((nbourdist M) . V,Q) + ((nbourdist M) . Q,W)
let V, Q, W be Element of M -neighbour ; :: thesis: (nbourdist M) . V,W <= ((nbourdist M) . V,Q) + ((nbourdist M) . Q,W)
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;
consider w being Element of M such that
A5: W = w -neighbour by Th23;
A6: w in W by A5, Th9;
A7: (nbourdist M) . V,Q = dist p,q by A2, A4, Def13;
A8: (nbourdist M) . V,W = dist p,w by A2, A6, Def13;
(nbourdist M) . Q,W = dist q,w by A4, A6, Def13;
hence (nbourdist M) . V,W <= ((nbourdist M) . V,Q) + ((nbourdist M) . Q,W) by A7, A8, METRIC_1:4; :: thesis: verum