let F be Field; for V being finite-dimensional VectSp of F
for k being Nat
for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
let V be finite-dimensional VectSp of F; for k being Nat
for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
let k be Nat; for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
let W1, W2, W be Subspace of V; ( W in pencil (W1,W2,k) implies ( W1 is Subspace of W & W is Subspace of W2 ) )
assume A1:
W in pencil (W1,W2,k)
; ( W1 is Subspace of W & W is Subspace of W2 )
then A2:
ex X being strict Subspace of V st
( W = X & dim X = k )
by VECTSP_9:def 2;
W in pencil (W1,W2)
by A1, XBOOLE_0:def 4;
then A3:
W in segment (W1,W2)
by XBOOLE_0:def 5;
then
W1 is Subspace of W2
by Def1;
hence
( W1 is Subspace of W & W is Subspace of W2 )
by A2, A3, Def1; verum