let a, b, c, d, e, f, g, h, i be Real; |{|[a,b,c]|,|[d,e,f]|,|[g,h,i]|}| = ((((((a * e) * i) + ((b * f) * g)) + ((c * d) * h)) - ((g * e) * c)) - ((h * f) * a)) - ((i * d) * b)
reconsider p = |[a,b,c]|, q = |[d,e,f]|, r = |[g,h,i]| as Element of (TOP-REAL 3) ;
A1:
( p `1 = a & p `2 = b & p `3 = c & q `1 = d & q `2 = e & q `3 = f & r `1 = g & r `2 = h & r `3 = i )
by EUCLID_5:2;
|{|[a,b,c]|,|[d,e,f]|,|[g,h,i]|}| = (((((((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 ANPROJ_8:27;
hence
|{|[a,b,c]|,|[d,e,f]|,|[g,h,i]|}| = ((((((a * e) * i) + ((b * f) * g)) + ((c * d) * h)) - ((g * e) * c)) - ((h * f) * a)) - ((i * d) * b)
by A1; verum