let V be RealLinearSpace; :: thesis: for A being Subset of V st Lin A = V holds

ex I being Basis of V st I c= A

let A be Subset of V; :: thesis: ( Lin A = V implies ex I being Basis of V st I c= A )

assume Lin A = V ; :: thesis: ex I being Basis of V st I c= A

then consider B being Subset of V such that

A1: B c= A and

A2: ( B is linearly-independent & Lin B = V ) by Th25;

reconsider B = B as Basis of V by A2, Def3;

take B ; :: thesis: B c= A

thus B c= A by A1; :: thesis: verum

ex I being Basis of V st I c= A

let A be Subset of V; :: thesis: ( Lin A = V implies ex I being Basis of V st I c= A )

assume Lin A = V ; :: thesis: ex I being Basis of V st I c= A

then consider B being Subset of V such that

A1: B c= A and

A2: ( B is linearly-independent & Lin B = V ) by Th25;

reconsider B = B as Basis of V by A2, Def3;

take B ; :: thesis: B c= A

thus B c= A by A1; :: thesis: verum