theorem Th13: :: EUCLID_8:13

for p being Element of REAL 3 holds |(p,|[0,0,0]|)| = 0