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