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