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 - u),(v - u)} 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 - u),(v - u)} is linearly-independent )
assume A1: ( {u,w,v} is linearly-independent & u <> v & u <> w & v <> w ) ; :: thesis: {u,(w - u),(v - u)} is linearly-independent

now :: thesis: for a, b, c being Real st ((a * u) + (b * (w - u))) + (c * (v - u)) = 0. V holds
( a = 0 & b = 0 & c = 0 )

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

end;

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