let GF be Field; :: thesis: for n being Nat
for V being finite-dimensional VectSp of GF st dim V < n holds
n Subspaces_of V = {}
let n be Nat; :: thesis: for V being finite-dimensional VectSp of GF st dim V < n holds
n Subspaces_of V = {}
let V be finite-dimensional VectSp of GF; :: thesis: ( dim V < n implies n Subspaces_of V = {} )
assume that
A1: dim V < n and
A2: n Subspaces_of V <> {} ; :: thesis: contradiction
consider x being object such that
A3: x in n Subspaces_of V by A2, XBOOLE_0:def 1;
ex W being strict Subspace of V st
( W = x & dim W = n ) by A3, Def2;
hence contradiction by A1, Th25; :: thesis: verum