theorem :: EUCLID_8:80

for p being Element of REAL 3 holds
( |.p.| = 0 iff p = 0.REAL 3 )