theorem :: RLVECT_X:36

for V being RealLinearSpace
for A being Subset of V holds Z_Lin (Z_Lin A) = Z_Lin A