let p be Point of (TOP-REAL 3); :: thesis: ( (0. (TOP-REAL 3)) <X> p = 0. (TOP-REAL 3) & p <X> (0. (TOP-REAL 3)) = 0. (TOP-REAL 3) )
A1: (0. (TOP-REAL 3)) <X> p = |[0,0,0]| <X> |[(p `1),(p `2),(p `3)]| by EUCLID_5:3, EUCLID_5:4
.= 0. (TOP-REAL 3) by EUCLID_5:19 ;
p <X> (0. (TOP-REAL 3)) = - (0. (TOP-REAL 3)) by A1, EUCLID_5:17
.= 0. (TOP-REAL 3) by RLVECT_1:12 ;
hence ( (0. (TOP-REAL 3)) <X> p = 0. (TOP-REAL 3) & p <X> (0. (TOP-REAL 3)) = 0. (TOP-REAL 3) ) by A1; :: thesis: verum