for x being set st x in X holds
x is finite by MATROID0:def 5;
hence union X is finite by FINSET_1:7; :: thesis: verum