let V be RealLinearSpace; :: thesis: 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 y is zero & not u,v,y are_LinDep )

let p, q, r be Element of V; :: thesis: ( 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 y is zero & not u,v,y are_LinDep ) )

assume A1: not p,q,r are_LinDep ; :: thesis: 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 y is zero & not u,v,y are_LinDep )

let u, v be Element of V; :: thesis: ( not u is zero & not v is zero & not are_Prop u,v implies ex y being Element of V st

( not y is zero & not u,v,y are_LinDep ) )

assume ( not u is zero & not v is zero & not are_Prop u,v ) ; :: thesis: ex y being Element of V st

( not y is zero & not u,v,y are_LinDep )

then consider y being Element of V such that

A2: not u,v,y are_LinDep by A1, Lm8;

take y ; :: thesis: ( not y is zero & not u,v,y are_LinDep )

thus not y is zero by A2, Th12; :: thesis: not u,v,y are_LinDep

thus not u,v,y are_LinDep by A2; :: thesis: verum

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 y is zero & not u,v,y are_LinDep )

let p, q, r be Element of V; :: thesis: ( 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 y is zero & not u,v,y are_LinDep ) )

assume A1: not p,q,r are_LinDep ; :: thesis: 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 y is zero & not u,v,y are_LinDep )

let u, v be Element of V; :: thesis: ( not u is zero & not v is zero & not are_Prop u,v implies ex y being Element of V st

( not y is zero & not u,v,y are_LinDep ) )

assume ( not u is zero & not v is zero & not are_Prop u,v ) ; :: thesis: ex y being Element of V st

( not y is zero & not u,v,y are_LinDep )

then consider y being Element of V such that

A2: not u,v,y are_LinDep by A1, Lm8;

take y ; :: thesis: ( not y is zero & not u,v,y are_LinDep )

thus not y is zero by A2, Th12; :: thesis: not u,v,y are_LinDep

thus not u,v,y are_LinDep by A2; :: thesis: verum