let F be Field; :: thesis: for a, b, c, d being Element of F holds ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F
let a, b, c, d be Element of F; :: thesis: ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F
( - (a - b) = b - a & - (c - d) = d - c ) by Lm1;
then ((a - b) * (c - d)) - ((b - a) * (d - c)) = ((a - b) * (c - d)) - ((a - b) * (c - d)) by VECTSP_1:10;
hence ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F by RLVECT_1:15; :: thesis: verum