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