take M ; :: according to CARD_1:def 4 :: thesis: nextcard M = nextcard M
thus nextcard M = nextcard M ; :: thesis: verum