let x1, x2, y1, y2, z1, z2 be Real; :: thesis: |[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]|
A1: ( |[x1,y1,z1]| `3 = z1 & |[x2,y2,z2]| `1 = x2 ) ;
A2: ( |[x2,y2,z2]| `2 = y2 & |[x2,y2,z2]| `3 = z2 ) ;
( |[x1,y1,z1]| `1 = x1 & |[x1,y1,z1]| `2 = y1 ) ;
hence |[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]| by A1, A2, Th12; :: thesis: verum