theorem Th13: :: EUCLID_5:13

for x1, x2, y1, y2, z1, z2 being Real holds |[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]|