theorem :: EUCLID_8:46

for x1, x2, x3, y1, y2, y3 being Real holds |[x1,x2,x3]| - |[y1,y2,y3]| = (((x1 - y1) * <e1>) + ((x2 - y2) * <e2>)) + ((x3 - y3) * <e3>)