let x, y, z be Real; :: thesis: |[0 ,0 ,0 ]| <X> |[x,y,z]| = 0. (TOP-REAL 3)
|[0 ,0 ,0 ]| <X> |[x,y,z]| = |[((0 * z) - (0 * y)),((0 * x) - (0 * z)),((0 * y) - (0 * x))]| by Th15
.= |[(0 * (z - y)),(0 * (x - z)),(0 * (y - x))]|
.= 0 * |[(z - y),(x - z),(y - x)]| by Th8 ;
hence |[0 ,0 ,0 ]| <X> |[x,y,z]| = 0. (TOP-REAL 3) by EUCLID:33; :: thesis: verum