let V be RealLinearSpace; :: thesis: for u, v, w being Element of V st ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) holds
w,u,v are_LinDep
let u, v, w be Element of V; :: thesis: ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )
A1: for u, v, w being Element of V st are_Prop u,v holds
w,u,v are_LinDep

proof

let u, v, w be Element of V; :: thesis: ( are_Prop u,v implies w,u,v are_LinDep )
A2: 0 * w = 0. V by RLVECT_1:10;
assume are_Prop u,v ; :: thesis: w,u,v are_LinDep
then consider a, b being Real such that
A3: a * u = b * v and
A4: a <> 0 and
b <> 0 ;
0. V = (a * u) + (- (b * v)) by A3, RLVECT_1:5
.= (a * u) + ((- 1) * (b * v)) by RLVECT_1:16
.= (a * u) + (((- 1) * b) * v) by RLVECT_1:def 7 ;
then 0. V = ((0 * w) + (a * u)) + (((- 1) * b) * v) by A2;
hence w,u,v are_LinDep by A4; :: thesis: verum

end;

A5: now :: thesis: ( are_Prop w,u & ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )

assume are_Prop w,u ; :: thesis: ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )
then v,w,u are_LinDep by A1;
hence ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep ) by Th5; :: thesis: verum

end;

A6: now :: thesis: ( are_Prop v,w & ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )

assume are_Prop v,w ; :: thesis: ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep )
then u,v,w are_LinDep by A1;
hence ( ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) implies w,u,v are_LinDep ) by Th5; :: thesis: verum

end;

assume ( are_Prop u,v or are_Prop w,u or are_Prop v,w ) ; :: thesis: w,u,v are_LinDep
hence w,u,v are_LinDep by A1, A5, A6; :: thesis: verum