let p, q, r be Point of (TOP-REAL 3); :: thesis: |{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))
A1: p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3;
A2: q <X> r = |[(((q `2) * (r `3)) - ((q `3) * (r `2))),(((q `3) * (r `1)) - ((q `1) * (r `3))),(((q `1) * (r `2)) - ((q `2) * (r `1)))]| by EUCLID_5:def 4;
|(p,(q <X> r))| = (((p `1) * (((q `2) * (r `3)) - ((q `3) * (r `2)))) + ((p `2) * (((q `3) * (r `1)) - ((q `1) * (r `3))))) + ((p `3) * (((q `1) * (r `2)) - ((q `2) * (r `1)))) by A1, A2, EUCLID_5:30;
hence |{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 EUCLID_5:def 5; :: thesis: verum