set a = the Element of the topology of M;
reconsider a = the Element of the topology of M as independent Subset of M by PRE_TOPC:def 2;
{} c= a ;
then reconsider b = {} as independent Subset of M by Th1;
take b ; :: thesis: ( b is finite & b is independent )
thus ( b is finite & b is independent ) ; :: thesis: verum