theorem :: EUCLID_8:95

for q, p1, p2 being Element of REAL 3 holds |{p1,p2,q}| = |((q <X> p1),p2)|