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