theorem Th20: :: ABCMIZ_1:20

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