let F be Field; :: thesis: for a, b, c, e, g, h being Element of F holds ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F
let a, b, c, e, g, h be Element of F; :: thesis: ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F
( c - ((c + h) + (- g)) = g - h & e - ((e + b) + (- a)) = a - b ) by Lm14;
hence ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F by RLVECT_1:15; :: thesis: verum