for V being RealUnitarySpace
for A, B being finite Subset of V st UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar 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) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )