let x1, x2 be Real; |[x1,0,0]| <X> |[x2,0,0]| = 0. (TOP-REAL 3)
|[x1,0,0]| <X> |[x2,0,0]| =
|[((0 * 0) - (0 * 0)),((0 * x2) - (x1 * 0)),((x1 * 0) - (0 * x2))]|
by Th15
.=
|[(0 * (0 - 0)),(0 * (x2 - x1)),(0 * (x1 - x2))]|
.=
0 * |[(0 - 0),(x2 - x1),(x1 - x2)]|
by Th8
.=
0. (TOP-REAL 3)
by RLVECT_1:10
;
hence
|[x1,0,0]| <X> |[x2,0,0]| = 0. (TOP-REAL 3)
; verum