let n be Nat; :: thesis: nextcard (card n) = card (n + 1)
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A1: for M being Cardinal st card (card n) in M holds
card (n + 1) c= M

proof

A2: card n = n by CARD_1:def 5;
let M be Cardinal; :: thesis: ( card (card n) in M implies card (n + 1) c= M )
assume card (card n) in M ; :: thesis: card (n + 1) c= M
then A3: succ n c= M by A2, ORDINAL1:33;
n + 1 = succ n by Th39;
hence card (n + 1) c= M by A3, CARD_1:def 5; :: thesis: verum

end;

n < n + 1 by Th13;
then card (card n) in card (n + 1) by Th42;
hence nextcard (card n) = card (n + 1) by A1, CARD_1:def 6; :: thesis: verum