X, card X are_equipotent by Def5;
hence not card X is finite by Th68; :: thesis: verum