let V be RealLinearSpace; :: thesis: for u, v, w being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,w,(- v)} is linearly-independent
let u, v, w be VECTOR of V; :: thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,w,(- v)} is linearly-independent )
- v = (- 1) * v by RLVECT_1:16;
hence ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,w,(- v)} is linearly-independent ) by Th27; :: thesis: verum