let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V
for a, b being Real holds (a - b) * (u - v) = (b - a) * (v - u)
let u, v be VECTOR of V; :: thesis: for a, b being Real holds (a - b) * (u - v) = (b - a) * (v - u)
let a, b be Real; :: thesis: (a - b) * (u - v) = (b - a) * (v - u)
thus (a - b) * (u - v) = (- (b - a)) * (- (v - u)) by RLVECT_1:33
.= (b - a) * (v - u) by RLVECT_1:26 ; :: thesis: verum