theorem Th7: :: ASCOLI2:7

for X being MetrSpace
for x, y, v, w being Element of X holds |.((dist (x,y)) - (dist (v,w))).| <= (dist (x,v)) + (dist (y,w))