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))]|
.= |[(0 * (z2 - z1)),(0 * (z1 - z2)),(0 * (0 * 0))]|
.= 0 * |[(z2 - z1),(z1 - z2),(0 - 0)]| by Th8
.= 0. (TOP-REAL 3) by RLVECT_1:10 ;
hence |[0,0,z1]| <X> |[0,0,z2]| = 0. (TOP-REAL 3) ; :: thesis: verum