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