let q, p1, p2 be Element of REAL 3; :: thesis: |{p1,p2,q}| = |((q <X> p1),p2)|
|{p1,p2,q}| = |{p2,q,p1}| by Th84;
hence |{p1,p2,q}| = |((q <X> p1),p2)| ; :: thesis: verum