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

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