for X being set st the_rank_of X is finite holds
X is finite