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