let V be RealLinearSpace; 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; ( ( u = 0. V or v = 0. V or w = 0. V ) implies u,v,w are_LinDep )
A1:
for u, v, w being Element of V st u = 0. V holds
u,v,w are_LinDep
assume
( u = 0. V or v = 0. V or w = 0. V )
; u,v,w are_LinDep
hence
u,v,w are_LinDep
by A1, A3, A4; verum