let n be Nat; :: thesis: nextcard (card n) = card (succ n)
reconsider sn = succ n as Nat ;
for M being Cardinal st card (card n) in M holds
card (succ n) c= M by ORDINAL1:21;
hence nextcard (card n) = card (succ n) by Def3, ORDINAL1:6; :: thesis: verum