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))]| 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 EUCLID:33 ;
hence |[x1,0 ,0 ]| <X> |[x2,0 ,0 ]| = 0. (TOP-REAL 3) ; :: thesis: verum