theorem Th15: :: RLAFFIN1:15

for V being RealLinearSpace
for A, B being Subset of V st A is linearly-independent & A c= B & Lin B = V holds
ex I being linearly-independent Subset of V st
( A c= I & I c= B & Lin I = V )