theorem Th18: :: RLVECT_3:18

for V being RealLinearSpace
for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W