theorem Th12: :: VECTSP_7:25
for R being domRing
for V being LeftMod of R
for A being Subset of V
for W being strict Subspace of V st not R is degenerated & A = the carrier of W holds
Lin A = W