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