let V be RealLinearSpace; :: thesis: for A being Subset of V holds Lin (Z_Lin A) = Lin A
let A be Subset of V; :: thesis: Lin (Z_Lin A) = Lin A
for x being set st x in A holds
x in Z_Lin A by Th18;
then A c= Z_Lin A by TARSKI:def 3;
then P2: Lin A is Subspace of Lin (Z_Lin A) by RLVECT_3:23;
reconsider W = the carrier of (Lin A) as Subset of V by RLSUB_1:def 2;
Lin (Z_Lin A) is Subspace of Lin W by RLVECT_3:23, LM004;
then Lin (Z_Lin A) is Subspace of Lin A by RLVECT_3:21;
hence Lin (Z_Lin A) = Lin A by P2, RLSUB_1:34; :: thesis: verum