let V be RealLinearSpace; for p, q, r being Element of V st not p,q,r are_LinDep holds
for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st not u,v,y are_LinDep
let p, q, r be Element of V; ( not p,q,r are_LinDep implies for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st not u,v,y are_LinDep )
assume A1:
not p,q,r are_LinDep
; for u, v being Element of V st not u is zero & not v is zero & not are_Prop u,v holds
ex y being Element of V st not u,v,y are_LinDep
let u, v be Element of V; ( not u is zero & not v is zero & not are_Prop u,v implies ex y being Element of V st not u,v,y are_LinDep )
assume A2:
( not u is zero & not v is zero & not are_Prop u,v )
; not for y being Element of V holds u,v,y are_LinDep
assume A3:
for y being Element of V holds u,v,y are_LinDep
; contradiction
then A4:
u,v,r are_LinDep
;
( u,v,p are_LinDep & u,v,q are_LinDep )
by A3;
hence
contradiction
by A1, A2, A4, Th14; verum