let y1, y2 be Real; :: thesis: |[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 EUCLID:33 ;
hence |[0 ,y1,0 ]| <X> |[0 ,y2,0 ]| = 0. (TOP-REAL 3) ; :: thesis: verum