let p, q, r be Point of (TOP-REAL 3); :: thesis: ( |{p,q,r}| = |{r,p,q}| & |{p,q,r}| = |{q,r,p}| )
thus |{p,q,r}| = - |{p,r,q}| by ANPROJ_8:29
.= |{r,p,q}| by ANPROJ_8:30 ; :: thesis: |{p,q,r}| = |{q,r,p}|
thus |{p,q,r}| = - |{q,p,r}| by ANPROJ_8:30
.= |{q,r,p}| by ANPROJ_8:29 ; :: thesis: verum