theorem Th22: :: RLVECT_5:22

for V being RealLinearSpace
for A, B being finite Subset of V st RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent holds
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) )