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