set A = the independent Subset of M;

set C = [#] M;

consider B being independent Subset of M such that

the independent Subset of M c= B and

A1: B is_maximal_independent_in [#] M by Th14;

take B ; :: thesis: B is_maximal_independent_in [#] M

thus B is_maximal_independent_in [#] M by A1; :: thesis: verum

set C = [#] M;

consider B being independent Subset of M such that

the independent Subset of M c= B and

A1: B is_maximal_independent_in [#] M by Th14;

take B ; :: thesis: B is_maximal_independent_in [#] M

thus B is_maximal_independent_in [#] M by A1; :: thesis: verum