let V be RealLinearSpace; :: thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
the carrier of (Lin V1) = V1
let V1 be Subset of V; :: thesis: ( V1 <> {} & V1 is linearly-closed implies the carrier of (Lin V1) = V1 )
assume ( V1 <> {} & V1 is linearly-closed ) ; :: thesis: the carrier of (Lin V1) = V1
then ex W0 being strict Subspace of V st V1 = the carrier of W0 by RLSUB_1:35;
hence the carrier of (Lin V1) = V1 by RLVECT_3:18; :: thesis: verum