X, card X are_equipotent by Def2;
hence not card X is finite by Th37; :: thesis: verum