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