let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for m being Nat st 1 <= m & m + 1 < dim V holds
GrassmannSpace V,m,(m + 1) is PLS
let V be finite-dimensional VectSp of F; :: thesis: for m being Nat st 1 <= m & m + 1 < dim V holds
GrassmannSpace V,m,(m + 1) is PLS
let m be Nat; :: thesis: ( 1 <= m & m + 1 < dim V implies GrassmannSpace V,m,(m + 1) is PLS )
assume that
A1: 1 <= m and
A2: m + 1 < dim V ; :: thesis: GrassmannSpace V,m,(m + 1) is PLS
A3: m < m + 1 by NAT_1:13;
m <= dim V by A2, NAT_1:13;
hence GrassmannSpace V,m,(m + 1) is PLS by A1, A2, A3, Th28, Th29, Th30, Th31, VECTSP_9:40; :: thesis: verum
set S = GrassmannSpace V,m,(m + 1);