for x being set st x in X holds
x is finite ;
hence union X is finite by Th7; :: thesis: verum