let V be non trivial RealLinearSpace; :: thesis: for u, v, w being Element of V holds
( u,v,w are_LinDep iff ( u = v or u = w or v = w or {u,v,w} is linearly-dependent ) )
let u, v, w be Element of V; :: thesis: ( u,v,w are_LinDep iff ( u = v or u = w or v = w or {u,v,w} is linearly-dependent ) )
hereby :: thesis: ( ( u = v or u = w or v = w or {u,v,w} is linearly-dependent ) implies u,v,w are_LinDep )
assume u,v,w are_LinDep ; :: thesis: ( u = v or u = w or v = w or {u,v,w} is linearly-dependent )
then ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) by ANPROJ_1:def 2;
hence ( u = v or u = w or v = w or {u,v,w} is linearly-dependent ) by RLVECT_4:7; :: thesis: verum
end;
assume ( u = v or u = w or v = w or {u,v,w} is linearly-dependent ) ; :: thesis: u,v,w are_LinDep
then ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) by RLVECT_4:7;
hence u,v,w are_LinDep by ANPROJ_1:def 2; :: thesis: verum