let V be RealLinearSpace; :: thesis: for u, v, w being Element of V st ( u = 0. V or v = 0. V or w = 0. V ) holds
u,v,w are_LinDep
let u, v, w be Element of V; :: thesis: ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )
assume A1: ( u = 0. V or v = 0. V or w = 0. V ) ; :: thesis: u,v,w are_LinDep
A2: for u, v, w being Element of V st u = 0. V holds
u,v,w are_LinDep

proof

let u, v, w be Element of V; :: thesis: ( u = 0. V implies u,v,w are_LinDep )
assume A3: u = 0. V ; :: thesis: u,v,w are_LinDep
0. V = (0. V) + (0. V) by RLVECT_1:10
.= (1 * u) + (0. V) by A3, RLVECT_1:23
.= (1 * u) + (0 * v) by RLVECT_1:23
.= ((1 * u) + (0 * v)) + (0. V) by RLVECT_1:10
.= ((1 * u) + (0 * v)) + (0 * w) by RLVECT_1:23 ;
hence u,v,w are_LinDep by Def3; :: thesis: verum

end;

A4: now

assume v = 0. V ; :: thesis: u,v,w are_LinDep
then v,w,u are_LinDep by A2;
hence u,v,w are_LinDep by Th10; :: thesis: verum

end;

now

assume w = 0. V ; :: thesis: u,v,w are_LinDep
then w,u,v are_LinDep by A2;
hence u,v,w are_LinDep by Th10; :: thesis: verum

end;

hence u,v,w are_LinDep by A1, A2, A4; :: thesis: verum