theorem Th8: :: RLVECT_X:8

for V being RealLinearSpace
for A being Subset of V holds Z_Lin A c= the carrier of (Lin A)