let V be RealLinearSpace; :: thesis: for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds
{u,w,(v - u)} is linearly-independent
let u, w, v be VECTOR of V; :: thesis: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u,w,(v - u)} is linearly-independent )
assume A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) ; :: thesis: {u,w,(v - u)} is linearly-independent

now

let a, b, c be Real; :: thesis: ( ((a * u) + (b * w)) + (c * (v - u)) = 0. V implies ( a = 0 & b = 0 & c = 0 ) )
assume ((a * u) + (b * w)) + (c * (v - u)) = 0. V ; :: thesis: ( a = 0 & b = 0 & c = 0 )
then A2: 0. V = ((a * u) + (b * w)) + ((c * v) - (c * u)) by RLVECT_1:34
.= (a * u) + ((b * w) + ((c * v) - (c * u))) by RLVECT_1:def 3
.= (a * u) + (((b * w) + (c * v)) - (c * u)) by RLVECT_1:def 3
.= (a * u) + (((b * w) - (c * u)) + (c * v)) by RLVECT_1:def 3
.= ((a * u) + ((b * w) - (c * u))) + (c * v) by RLVECT_1:def 3
.= (((a * u) + (b * w)) - (c * u)) + (c * v) by RLVECT_1:def 3
.= (((a * u) - (c * u)) + (b * w)) + (c * v) by RLVECT_1:def 3
.= (((a - c) * u) + (b * w)) + (c * v) by RLVECT_1:35 ;
then a - c = 0 by A1, Th10;
hence ( a = 0 & b = 0 & c = 0 ) by A1, A2, Th10; :: thesis: verum

end;

hence {u,w,(v - u)} is linearly-independent by Th10; :: thesis: verum