let p, q, r be Point of (TOP-REAL 3); :: thesis: |{p,q,r}| = - |{q,p,r}|
A1: |{p,q,r}| = (((((((p `1) * (q `2)) * (r `3)) - (((p `3) * (q `2)) * (r `1))) - (((p `1) * (q `3)) * (r `2))) + (((p `2) * (q `3)) * (r `1))) - (((p `2) * (q `1)) * (r `3))) + (((p `3) * (q `1)) * (r `2)) by Th23;
|{q,p,r}| = (((((((q `1) * (p `2)) * (r `3)) - (((q `3) * (p `2)) * (r `1))) - (((q `1) * (p `3)) * (r `2))) + (((q `2) * (p `3)) * (r `1))) - (((q `2) * (p `1)) * (r `3))) + (((q `3) * (p `1)) * (r `2)) by Th23;
hence |{p,q,r}| = - |{q,p,r}| by A1; :: thesis: verum