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, Th25, Th26, Th27, Th28, VECTSP_9:36; :: thesis: verum