:: deftheorem defines GrassmannSpace PENCIL_4:def 7 :
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat holds GrassmannSpace (V,m,n) = TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #);