let p, q, r be Point of (TOP-REAL 3); :: thesis: for M being Matrix of 3,F_Real st M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> holds
|{p,q,r}| = Det M
let M be Matrix of 3,F_Real; :: thesis: ( M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> implies |{p,q,r}| = Det M )
assume A1: M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> ; :: thesis: |{p,q,r}| = Det M
A2: p = |[(p `1),(p `2),(p `3)]| by EUCLID_5:3;
A3: 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;
A4: |(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 A2, A3, EUCLID_5:30;
reconsider p1 = p `1 , p2 = p `2 , p3 = p `3 , q1 = q `1 , q2 = q `2 , q3 = q `3 , r1 = r `1 , r2 = r `2 , r3 = r `3 as Element of F_Real by XREAL_0:def 1;
Det M = ((((((p1 * q2) * r3) - ((p3 * q2) * r1)) - ((p1 * q3) * r2)) + ((p2 * q3) * r1)) - ((p2 * q1) * r3)) + ((p3 * q1) * r2) by A1, MATRIX_9:46;
hence |{p,q,r}| = Det M by A4, EUCLID_5:def 5; :: thesis: verum