theorem Th11: :: RUSUB_3:11

for V being RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )