let x1, x2 be Real; :: thesis: |[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))]|
.= |[(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) ; :: thesis: verum