assume A1: predecessor M is finite ; :: thesis: contradiction
M = nextcard (predecessor M) by Def17;
hence contradiction by A1, CARD_1:45; :: thesis: verum