theorem :: EUCLID_8:89

for p1, p2, p3 being Element of REAL 3 holds p1 <X> (p2 <X> p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3)