theorem :: EUCLID_8:22

for p being Element of REAL 3 holds p <X> |[0,0,0]| = |[0,0,0]|