theorem :: EUCLID_8:71

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