theorem :: RLVECT_3:19

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