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