let F be Field; for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m & m < n & n < dim V holds
not GrassmannSpace (V,m,n) is degenerated
let V be finite-dimensional VectSp of F; for m, n being Nat st 1 <= m & m < n & n < dim V holds
not GrassmannSpace (V,m,n) is degenerated
let m, n be Nat; ( 1 <= m & m < n & n < dim V implies not GrassmannSpace (V,m,n) is degenerated )
assume that
A1:
1 <= m
and
A2:
m < n
and
A3:
n < dim V
; not GrassmannSpace (V,m,n) is degenerated
set S = GrassmannSpace (V,m,n);
A4:
m < dim V
by A2, A3, XXREAL_0:2;
hereby PENCIL_1:def 5 verum
assume A5:
the
carrier of
(GrassmannSpace (V,m,n)) is
Block of
(GrassmannSpace (V,m,n))
;
contradiction
not the
topology of
(GrassmannSpace (V,m,n)) is
empty
by A3, Th22;
then consider W being
Subspace of
V such that A6:
dim W = n
and A7:
m Subspaces_of V = m Subspaces_of W
by A5, Def6;
(Omega). V = (Omega). W
by A1, A4, A7, Th24;
then
dim W = dim ((Omega). V)
by VECTSP_9:27;
hence
contradiction
by A3, A6, VECTSP_9:27;
verum
end;