let F be Field; :: thesis: for V being VectSp of
for A being Subset of holds
( A is independent iff A is linearly-independent Subset of )
let V be VectSp of ; :: thesis: for A being Subset of holds
( A is independent iff A is linearly-independent Subset of )
set M = LinearlyIndependentSubsets V;
let B be Subset of ; :: thesis: ( B is independent iff B is linearly-independent Subset of )
the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of : A is linearly-independent } by Def9;
then ( B in the_family_of (LinearlyIndependentSubsets V) iff ex A being Subset of st
( B = A & A is linearly-independent ) ) ;
hence ( B is independent iff B is linearly-independent Subset of ) by Def2; :: thesis: verum