theorem Th70: :: EUCLID_8:79

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