theorem :: EUCLID_8:3

for p1, p2 being Element of REAL 3 st p1,p2 are_ldependent2 holds
p1 <X> p2 = 0.REAL 3