let V be RealLinearSpace; for u, v, w being Element of V st u,v,w are_LinDep holds
( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep )
let u, v, w be Element of V; ( u,v,w are_LinDep implies ( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep ) )
assume
u,v,w are_LinDep
; ( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep )
then consider a, b, c being Real such that
A1:
((a * u) + (b * v)) + (c * w) = 0. V
and
A2:
( a <> 0 or b <> 0 or c <> 0 )
;
( ((a * u) + (c * w)) + (b * v) = 0. V & ((b * v) + (c * w)) + (a * u) = 0. V )
by A1, RLVECT_1:def 3;
hence
( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep )
by A1, A2; verum